Theorem Nat.one_lt_of_mem_properDivisors

Modification history

2023-12-25 12:41
Mathlib/NumberTheory/Divisors.lean
feat: add some missing API lemmas about `Nat.properDivisors` and `Nat.primeFactors` (#8858)
Added Nat.one_lt_of_mem_properDivisorsView on Github →