Theorem MulEquivClass.apply_coe_symm_apply

Modification history

2024-10-04 17:27
Mathlib/Algebra/Group/Equiv/Basic.lean
feat(Algebra/Group/Equiv): add two simp lemmas for `MulEquivClass` (#17085) …
Added MulEquivClass.apply_coe_symm_applyView on Github →