Def WithVal.valueGroupOrderIso₀

Modification history

2026-09-16 13:44

Mathlib/Topology/Algebra/Valued/WithVal.lean

fix(Algebra/MonoidWithZeroHom): normalize to `.toMonoidWithZeroHom` (#43728) …

Modified WithVal.valueGroupOrderIso₀ View on Github →

2026-06-06 05:44

Mathlib/Topology/Algebra/Valued/WithVal.lean

fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom (#36911) …

Modified WithVal.valueGroupOrderIso₀ View on Github →

2026-05-28 09:20

Mathlib/Topology/Algebra/Valued/WithVal.lean

feat: `algebraMap K L` is uniform continuous with respect to adic topologies, when the ideal `w` of `L` lies above `v` (#34045) …

Modified WithVal.valueGroupOrderIso₀ View on Github →

2026-03-06 13:45

Mathlib/Topology/Algebra/Valued/WithVal.lean

chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …

Added WithVal.valueGroupOrderIso₀ View on Github →