Theorem Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe

Modification history

2026-07-17 09:57

Mathlib/RingTheory/Valuation/Integers.lean

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

Deleted Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe 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.integer.coe_span_singleton_eq_setOf_le_v_coe View on Github →