Commit 2024-12-09 17:33 2c7acde6

View on Github →

chore(Module/LocalizedModule): rename ringHom_ext to ext (#19787) IsLocalizedModule.ringHom_ext does not have any RingHom in its type signature.

Estimated changes

Modified Mathlib/Algebra/Module/FinitePresentation.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

added theorem IsLocalizedModule.ext

deleted theorem IsLocalizedModule.ringHom_ext

Modified Mathlib/RingTheory/LocalProperties/Projective.lean