Commit 2023-12-25 12:41 60af8c9a

View on Github →

feat: add some missing API lemmas about Nat.properDivisors and Nat.primeFactors (#8858)

Estimated changes

Modified Mathlib/Data/Nat/PrimeFin.lean

added theorem Nat.nonempty_primeFactors

Modified Mathlib/NumberTheory/Divisors.lean

added theorem Nat.divisors_eq_empty

added theorem Nat.mem_properDivisors_iff_exists

added theorem Nat.nonempty_divisors

added theorem Nat.nonempty_properDivisors

added theorem Nat.one_lt_div_of_mem_properDivisors

added theorem Nat.one_lt_of_mem_properDivisors

added theorem Nat.properDivisors_eq_empty