Commit 2026-09-24 13:25 48714044

View on Github →

chore(RingTheory/Valuation/DiscreteValuativeRel): fix two typos in lemma name (#43587)

Estimated changes

Modified Mathlib/NumberTheory/LocalField/Basic.lean

Modified Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean

added theorem ValuativeRel.ValueGroupWithZero.nonempty_orderMonoidIso_withZeroMulInt_iff

deleted theorem ValuativeRel.nonempty_orderIso_withZeroMul_int_iff