basic): add `ite_one_mul` and `ite_zero_add` (#9227)

Commit

4 years ago

chore(algebra/group/basic): add `ite_one_mul` and `ite_zero_add` (#9227) We already had the versions with the arguments in the other order. Follows on from #3217

Author

eric-wieser

Parents

18d031d1

mathlib3 5b75f5ac - chore(algebra/group/basic): add `ite_one_mul` and `ite_zero_add` (#9227)

mathlib3
5b75f5ac - chore(algebra/group/basic): add `ite_one_mul` and `ite_zero_add` (#9227)