Theorem Ideal.IsPrime.notMem_of_isCoprime_of_mem

Modification history

2025-11-17 14:01

Mathlib/RingTheory/Ideal/Operations.lean

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

Added Ideal.IsPrime.notMem_of_isCoprime_of_mem View on Github →