Theorem Nat.Prime.dvd_iff_one_le_factorization

Modification history