Theorem IsCoprime.isUnit_of_associated

Modification history

2026-03-06 21:32
Mathlib/RingTheory/Coprime/Basic.lean
feat(FieldTheory/RatFunc): Lüroth's theorem (#36109)
Added IsCoprime.isUnit_of_associatedView on Github →