Commit 2024-07-03 09:27 bb3c3427

View on Github →

feat (RingTheory/Valuation) : add lemmas about valuations and notations for valued (#13533) Add related lemmas about valuations. Add notations for integer, maximal ideal and residue field for valued field. Relocate files concerning Valued under a new folder Topology/Algebra/Valued.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/FunctionField.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/Ideal/LocalRing.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.one_le_val_iff

added theorem Valuation.val_eq_one_iff

added theorem Valuation.val_le_one_iff

added theorem Valuation.val_le_one_or_val_inv_le_one

added theorem Valuation.val_le_one_or_val_inv_lt_one

added theorem Valuation.val_lt_one_iff

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.eq_algebraMap_or_inv_eq_algebraMap

added theorem Valuation.Integers.isUnit_of_one'

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

added theorem ValuationRing.isFractionRing_iff

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Renamed Mathlib/Topology/Algebra/NormedValued.lean to Mathlib/Topology/Algebra/Valued/NormedValued.lean

Renamed Mathlib/Topology/Algebra/Valuation.lean to Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

Renamed Mathlib/Topology/Algebra/ValuedField.lean to Mathlib/Topology/Algebra/Valued/ValuedField.lean

added def Valued.ResidueField

added def Valued.integer

added def Valued.maximalIdeal