Commit 2025-07-08 21:40 fb6a587d

View on Github →

feat(Valuation/RankOne): equivalence with ValuativeRel.isRankLeOne (#26754) refactor to have Valuation.RankOne extend the new Valuation.IsNontrivial and characterization iffs for ValuativeRel.IsNontrivial relating to units of value group, or Valuation.IsNontrivial

Estimated changes

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Modified Mathlib/NumberTheory/Padics/Complex.lean

Modified Mathlib/RingTheory/Valuation/RankOne.lean

modified theorem Valuation.RankOne.nontrivial

added def Valuation.RankOne.ofRankLeOneStruct

added def Valuation.RankOne.rankLeOneStruct

added theorem ValuativeRel.isNontrivial_of_rankOne

added theorem ValuativeRel.isRankLeOne_of_rankOne

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_one

added theorem ValuativeRel.isNontrivial_iff_isNontrivial

added theorem ValuativeRel.isNontrivial_iff_nontrivial_units

modified theorem ValuativeRel.rel_mul

added theorem ValuativeRel.rel_trans'

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean