Theorem MulEquivClass.coe_symm_apply_apply

Modification history

2025-01-15 21:51
Mathlib/Algebra/Group/Equiv/Basic.lean
chore(Algebra/Group/Equiv): split into `Defs` and `Basic` (#20712) …
Modified MulEquivClass.coe_symm_apply_applyView on Github →
2024-10-04 17:27
Mathlib/Algebra/Group/Equiv/Basic.lean
feat(Algebra/Group/Equiv): add two simp lemmas for `MulEquivClass` (#17085) …
Added MulEquivClass.coe_symm_apply_applyView on Github →