Commit 2025-08-27 13:41 0b2425fe

View on Github →

chore(RingTheory/Valuation): move ValuativeRel to ValuativeRel.Basic (#28890) in preparation for trivial rel and discrete rel files like in #27313

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Valuation/RankOne.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

deleted theorem Valuation.Compatible.ofValuation

deleted theorem Valuation.apply_posSubmonoid_ne_zero

deleted theorem Valuation.apply_posSubmonoid_pos

deleted def ValuativeExtension.mapPosSubmonoid

deleted def ValuativeExtension.mapValueGroupWithZero

deleted theorem ValuativeExtension.mapValueGroupWithZero_mk

deleted theorem ValuativeExtension.mapValueGroupWithZero_valuation

deleted structure ValuativeRel.RankLeOneStruct

deleted theorem ValuativeRel.ValueGroupWithZero.bot_eq_zero

deleted def ValuativeRel.ValueGroupWithZero.embed

deleted theorem ValuativeRel.ValueGroupWithZero.embed_mk

deleted theorem ValuativeRel.ValueGroupWithZero.embed_strictMono

deleted theorem ValuativeRel.ValueGroupWithZero.embed_valuation

deleted theorem ValuativeRel.ValueGroupWithZero.exact

deleted theorem ValuativeRel.ValueGroupWithZero.ind

deleted theorem ValuativeRel.ValueGroupWithZero.inv_mk

deleted def ValuativeRel.ValueGroupWithZero.lift

deleted theorem ValuativeRel.ValueGroupWithZero.lift_mk

deleted theorem ValuativeRel.ValueGroupWithZero.lift_mul

deleted theorem ValuativeRel.ValueGroupWithZero.lift_one

deleted theorem ValuativeRel.ValueGroupWithZero.lift_valuation

deleted theorem ValuativeRel.ValueGroupWithZero.lift_zero

deleted def ValuativeRel.ValueGroupWithZero.lift₂

deleted theorem ValuativeRel.ValueGroupWithZero.lift₂_mk

deleted def ValuativeRel.ValueGroupWithZero.mk

deleted theorem ValuativeRel.ValueGroupWithZero.mk_eq_div

deleted theorem ValuativeRel.ValueGroupWithZero.mk_eq_mk

deleted theorem ValuativeRel.ValueGroupWithZero.mk_eq_one

deleted theorem ValuativeRel.ValueGroupWithZero.mk_eq_zero

deleted theorem ValuativeRel.ValueGroupWithZero.mk_le_mk

deleted theorem ValuativeRel.ValueGroupWithZero.mk_lt_mk

deleted theorem ValuativeRel.ValueGroupWithZero.mk_mul_mk

deleted theorem ValuativeRel.ValueGroupWithZero.mk_one_one

deleted theorem ValuativeRel.ValueGroupWithZero.mk_self

deleted theorem ValuativeRel.ValueGroupWithZero.mk_zero

deleted theorem ValuativeRel.ValueGroupWithZero.sound

deleted def ValuativeRel.ValueGroupWithZero

deleted def ValuativeRel.WithPreorder

deleted theorem ValuativeRel.isEquiv

deleted theorem ValuativeRel.isNontrivial_iff_isNontrivial

deleted theorem ValuativeRel.isNontrivial_iff_nontrivial_units

deleted theorem ValuativeRel.left_cancel_posSubmonoid

deleted def ValuativeRel.ofValuation

deleted def ValuativeRel.posSubmonoid

deleted theorem ValuativeRel.posSubmonoid_def

deleted theorem ValuativeRel.rel_add_cases

deleted theorem ValuativeRel.rel_mul

deleted theorem ValuativeRel.rel_mul_left

deleted theorem ValuativeRel.rel_refl

deleted theorem ValuativeRel.rel_rfl

deleted theorem ValuativeRel.rel_trans'

deleted theorem ValuativeRel.right_cancel_posSubmonoid

deleted def ValuativeRel.supp

deleted theorem ValuativeRel.supp_def

deleted theorem ValuativeRel.supp_eq_valuation_supp

deleted theorem ValuativeRel.val_posSubmonoid_ne_zero

deleted def ValuativeRel.valuation

deleted theorem ValuativeRel.valuation_eq_zero_iff

deleted theorem ValuativeRel.valuation_posSubmonoid_ne_zero

deleted theorem ValuativeRel.valuation_surjective

deleted def ValuativeRel.valueSetoid

deleted theorem ValuativeRel.zero_rel

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

added theorem Valuation.Compatible.ofValuation

added theorem Valuation.apply_posSubmonoid_ne_zero

added theorem Valuation.apply_posSubmonoid_pos

added def ValuativeExtension.mapPosSubmonoid

added def ValuativeExtension.mapValueGroupWithZero

added theorem ValuativeExtension.mapValueGroupWithZero_mk

added theorem ValuativeExtension.mapValueGroupWithZero_valuation

added structure ValuativeRel.RankLeOneStruct

added theorem ValuativeRel.ValueGroupWithZero.bot_eq_zero

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.exact

added theorem ValuativeRel.ValueGroupWithZero.ind

added theorem ValuativeRel.ValueGroupWithZero.inv_mk

added def ValuativeRel.ValueGroupWithZero.lift

added theorem ValuativeRel.ValueGroupWithZero.lift_mk

added theorem ValuativeRel.ValueGroupWithZero.lift_mul

added theorem ValuativeRel.ValueGroupWithZero.lift_one

added theorem ValuativeRel.ValueGroupWithZero.lift_valuation

added theorem ValuativeRel.ValueGroupWithZero.lift_zero

added def ValuativeRel.ValueGroupWithZero.lift₂

added theorem ValuativeRel.ValueGroupWithZero.lift₂_mk

added def ValuativeRel.ValueGroupWithZero.mk

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_div

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_mk

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_one

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_zero

added theorem ValuativeRel.ValueGroupWithZero.mk_le_mk

added theorem ValuativeRel.ValueGroupWithZero.mk_lt_mk

added theorem ValuativeRel.ValueGroupWithZero.mk_mul_mk

added theorem ValuativeRel.ValueGroupWithZero.mk_one_one

added theorem ValuativeRel.ValueGroupWithZero.mk_self

added theorem ValuativeRel.ValueGroupWithZero.mk_zero

added theorem ValuativeRel.ValueGroupWithZero.sound

added def ValuativeRel.ValueGroupWithZero

added def ValuativeRel.WithPreorder

added theorem ValuativeRel.isEquiv

added theorem ValuativeRel.isNontrivial_iff_isNontrivial

added theorem ValuativeRel.isNontrivial_iff_nontrivial_units

added theorem ValuativeRel.left_cancel_posSubmonoid

added def ValuativeRel.ofValuation

added def ValuativeRel.posSubmonoid

added theorem ValuativeRel.posSubmonoid_def

added theorem ValuativeRel.rel_add_cases

added theorem ValuativeRel.rel_mul

added theorem ValuativeRel.rel_mul_left

added theorem ValuativeRel.rel_refl

added theorem ValuativeRel.rel_rfl

added theorem ValuativeRel.rel_trans'

added theorem ValuativeRel.right_cancel_posSubmonoid

added def ValuativeRel.supp

added theorem ValuativeRel.supp_def

added theorem ValuativeRel.supp_eq_valuation_supp

added theorem ValuativeRel.val_posSubmonoid_ne_zero

added def ValuativeRel.valuation

added theorem ValuativeRel.valuation_eq_zero_iff

added theorem ValuativeRel.valuation_posSubmonoid_ne_zero

added theorem ValuativeRel.valuation_surjective

added def ValuativeRel.valueSetoid

added theorem ValuativeRel.zero_rel

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

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