Commit 2026-05-12 14:07 54a8de26

View on Github →

chore: syntactically generalise symm_mk (#37748)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified theorem AlgEquiv.symm_mk

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

modified theorem LinearEquiv.symm_mk

Modified Mathlib/Algebra/Ring/Equiv.lean

modified theorem RingEquiv.symm_mk

Modified Mathlib/Algebra/Star/StarAlgHom.lean

modified theorem StarAlgEquiv.symm_mk

Modified Mathlib/Algebra/Star/StarRingHom.lean

modified theorem StarRingEquiv.symm_mk

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem Equiv.symm_mk

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/Polynomial/Quotient.lean

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

Modified Mathlib/RingTheory/TensorProduct/Free.lean