Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit.strongly_measurable_const_smul_iff

Modification history

2023-05-24 15:42

src/measure_theory/function/strongly_measurable/basic.lean

feat(measure_theory/function/strongly_measurable/basic): generalize to `is_unit c` from `c ≠ 0` (#19081) …

Added is_unit.strongly_measurable_const_smul_iff View on Github →