Theorem Nat.gcd_eq_one_of_lt_minFac

Modification history

2025-03-17 01:20
Mathlib/Data/Nat/Prime/Basic.lean
feat: add some elementary number theory lemmas (#22989) …
Added Nat.gcd_eq_one_of_lt_minFacView on Github →