Commit 2022-04-11 09:27 706905c5

View on Github →

fix(algebra/indicator_function): fix name of mul_indicator_eq_one_iff (#13284) It is about ≠, so call it mul_indicator_ne_one_iff/indicator_ne_zero_iff.

Estimated changes

Modified src/algebra/indicator_function.lean

added theorem set.mul_indicator_apply_ne_one

deleted theorem set.mul_indicator_eq_one_iff

Modified src/measure_theory/measure/measure_space_def.lean

Modified src/measure_theory/probability_mass_function/constructions.lean

modified theorem pmf.mem_support_filter_iff