mathlib3
706905c5 - fix(algebra/indicator_function): fix name of `mul_indicator_eq_one_iff` (#13284)

Commit

3 years ago

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`.

Author

urkud

Parents

ff507a35

mathlib3 706905c5 - fix(algebra/indicator_function): fix name of `mul_indicator_eq_one_iff` (#13284)

mathlib3
706905c5 - fix(algebra/indicator_function): fix name of `mul_indicator_eq_one_iff` (#13284)