Theorem Irreducible.gcd_eq_one_iff

Modification history

2023-10-02 06:27
Mathlib/Algebra/GCDMonoid/Basic.lean
feat: some lemmas about associated and prime elements (#7453) …
Added Irreducible.gcd_eq_one_iffView on Github →