Commit 2025-06-06 20:05 2b5cc7db

View on Github →

style: rename Submodule.MapSubtype.relIso to Submodule.MapSubtype.orderIso (#25374) Since OrderIso is an abbreviation of RelIso, we should rename Submodule.MapSubtype.relIso to Submodule.MapSubtype.orderIso.

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Range.lean

added def Submodule.MapSubtype.orderIso

deleted def Submodule.MapSubtype.relIso

Modified Mathlib/RingTheory/SimpleModule/Isotypic.lean