Theorem Rat.isCoprime_num_den

Modification history

2025-11-17 14:01

Mathlib/RingTheory/Coprime/Lemmas.lean

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

Added Rat.isCoprime_num_den View on Github →