Commit 2025-08-29 08:29 ac6d999f

View on Github →

feat(Algebra/Equiv): e.trans e.symm = refl (#29096) From Toric

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified theorem AlgEquiv.refl_toAlgHom

added theorem AlgEquiv.refl_toRingHom

added theorem AlgEquiv.self_trans_symm

added theorem AlgEquiv.symm_trans_self

added theorem AlgEquiv.toRingHom_trans