Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.factorization_prime_le_iff_dvd

Modification history

2022-12-22 09:08
src/data/nat/factorization/basic.lean
feat(group_theory/order_of_element): a condition on o(x) and o(y) that implies o(xy)=o(y) (#17997) …
Added nat.factorization_prime_le_iff_dvdView on Github →