Commit 2023-03-23 14:47 fa1b54f8

View on Github →

fix: add back lemmas deleted during porting (#3035) These lemmas are not tautologies, despite the assumption that they were. We know this because otherwise CI would fail. After adding these back, a few statements downstream need to change from statements about toEquiv to statements about EquivLike.toEquiv.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added def AlgEquiv.Simps.toEquiv

added theorem AlgEquiv.coe_ringEquiv'

deleted theorem AlgEquiv.coe_ring_equiv'

modified theorem AlgEquiv.symm_toEquiv_eq_symm

added theorem AlgEquiv.toEquiv_eq_coe

Modified Mathlib/Algebra/Group/Opposite.lean

modified theorem AddOpposite.opMulEquiv_toEquiv

modified theorem MulOpposite.opAddEquiv_toEquiv

Modified Mathlib/Algebra/Group/WithOne/Basic.lean

deleted theorem AddEquiv.withZeroCongr_apply

deleted theorem MulEquiv.withOneCongr_apply

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

modified theorem MulEquiv.coe_toEquiv

modified theorem MulEquiv.coe_toEquiv_symm

added theorem MulEquiv.toEquiv_eq_coe

modified theorem MulEquiv.toEquiv_symm

Modified Mathlib/Algebra/Hom/Equiv/Units/Basic.lean

deleted theorem MulEquiv.inv_apply

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

added theorem RingEquiv.toEquiv_eq_coe

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean