Commit 2025-07-31 23:29 2986ee04

View on Github →

feat(RingTheory/ValuativeRel): IsRankLeOne when there is a compatible Zm0 or NNReal valuation (#27183) and then provide it for Q_[p]

Estimated changes

Modified Mathlib/NumberTheory/Padics/ValuativeRel.lean

Modified Mathlib/RingTheory/Valuation/RankOne.lean

added theorem ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

modified def ValuativeExtension.mapValueGroupWithZero

added theorem ValuativeExtension.mapValueGroupWithZero_mk

added def ValuativeRel.ValueGroupWithZero.embed

added theorem ValuativeRel.ValueGroupWithZero.embed_mk

added theorem ValuativeRel.ValueGroupWithZero.embed_strictMono

added theorem ValuativeRel.ValueGroupWithZero.embed_valuation

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_div

added theorem ValuativeRel.val_posSubmonoid_ne_zero

added theorem ValuativeRel.valuation_eq_zero_iff

added theorem ValuativeRel.valuation_posSubmonoid_ne_zero

added theorem ValuativeRel.valuation_posSubmonoid_ne_zero_of_compatible