Commit 2020-10-04 11:10 231271d3

View on Github →

chore(data/equiv/mul_add): add more equiv lemmas to mul_equiv namespace (#4380) Also make apply_eq_iff_eq and apply_eq_iff_eq_symm_apply use implicit arguments.

Estimated changes

Modified src/category_theory/limits/types.lean

Modified src/data/equiv/basic.lean

modified theorem equiv.apply_eq_iff_eq

modified theorem equiv.apply_eq_iff_eq_symm_apply

Modified src/data/equiv/encodable/basic.lean

Modified src/data/equiv/mul_add.lean

added theorem mul_equiv.apply_eq_iff_eq

added theorem mul_equiv.apply_eq_iff_symm_apply

added theorem mul_equiv.eq_symm_apply

added theorem mul_equiv.symm_apply_eq

Modified src/data/opposite.lean

Modified src/group_theory/monoid_localization.lean