Theorem Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap

Modification history

2026-07-17 09:57

Mathlib/RingTheory/Valuation/Integers.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap View on Github →

2025-07-06 22:36

Mathlib/RingTheory/Valuation/Integers.lean

chore(RingTheory/Valuation): generalize lemmas about valuation of irreducibles in subring (#26545) …

Added Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap View on Github →