Commit 2025-10-01 10:14 79a12833

View on Github →

feat(FractionRing): add algHom_commutes (#29907) Add a version of algHom.commutes and algEquiv.commutes for fraction fields and use them to simplify some proofs.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem IsFractionRing.algEquiv_commutes

added theorem IsFractionRing.algHom_commutes