Commit 2025-09-29 16:33 d2669375

View on Github →

feat(RingTheory/ValuativeRel/Trivial): the trivial valuative relation (#27313) lemmas stated using [Valuation.Compatible (1 : Valuation R Γ₀)]

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupWithZero/Hom.lean

added theorem MonoidWithZeroHom.one_apply_eq_one_iff

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.one_apply_eq_one_iff

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

added theorem ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq

added theorem ValuativeRel.one_apply_posSubmonoid

Created Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean

added theorem ValuativeRel.eq_trivialRel_of_compatible_one

added theorem ValuativeRel.isDiscrete_trivialRel

added theorem ValuativeRel.not_isNontrivial_of_trivialRel

added theorem ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel

added def ValuativeRel.trivialRel

added theorem ValuativeRel.trivialRel_eq_ofValuation_one