Commit 2025-07-06 22:36 b368a619

View on Github →

chore(RingTheory/Valuation): generalize lemmas about valuation of irreducibles in subring (#26545) To prepare for generalization of LocallyCompact to Valued from NormedField

Estimated changes

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

added theorem Irreducible.maximalIdeal_eq_setOf_le_v_coe

added theorem Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow

added theorem Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap

added theorem Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap

added theorem Valuation.Integers.valuation_irreducible_lt_one

added theorem Valuation.Integers.valuation_irreducible_pos

added theorem Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe

added theorem Valuation.integer.v_irreducible_lt_one

added theorem Valuation.integer.v_irreducible_pos

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