Commit 2025-11-17 14:01 77bb8d0d

View on Github →

feat(DedekindDomain/AdicValuation): le_one lemmas for HeightOneSpectrum.valuation and specialisations to Rat (#30171)

Estimated changes

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

added theorem Rat.isCoprime_num_den

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff

added theorem Rat.valuation_le_one_iff_den

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.IsPrime.notMem_of_isCoprime_of_mem