mathlib
ef95945c
- feat(measure_theory/function/strongly_measurable/basic): generalize to `is_unit c` from `c ≠ 0` (#19081)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
feat(measure_theory/function/strongly_measurable/basic): generalize to `is_unit c` from `c ≠ 0` (#19081) We already have this generalization for `measurable_const_smul_iff` and `ae_measurable_const_smul_iff`.
References
lean-3.51.0
Author
eric-wieser
Parents
0372d31f
Loading