Def OrderMonoidIso.unitsCongr

Modification history

2026-05-28 09:20
Mathlib/Algebra/Order/Hom/Units.lean
feat: `algebraMap K L` is uniform continuous with respect to adic topologies, when the ideal `w` of `L` lies above `v` (#34045) …
Modified OrderMonoidIso.unitsCongrView on Github →
2025-08-22 16:06
Mathlib/Algebra/Order/Hom/Units.lean
feat(Algebra/Order): two auxiliary definitions (#28667) …
Added OrderMonoidIso.unitsCongrView on Github →