Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 11:38 dacf0490

View on Github →

feat(algebra/*): coe_to_equiv_symm simp lemmas (#12996)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.to_equiv_eq_coe

Modified src/algebra/hom/equiv.lean

modified theorem mul_equiv.coe_to_equiv

added theorem mul_equiv.to_equiv_eq_coe

Modified src/algebra/module/equiv.lean

added theorem linear_equiv.coe_to_equiv_symm

Modified src/group_theory/commensurable.lean