Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-01 16:43 7767ef8b

View on Github →

feat(number_theory/divisors): defines the finsets of divisors/proper divisors, perfect numbers, etc. (#4310) Defines nat.divisors n to be the set of divisors of n, and nat.proper_divisors to be the set of divisors of n other than n. Defines nat.divisors_antidiagonal in analogy to other antidiagonals used to define convolutions Defines nat.perfect, the predicate for perfect numbers

Estimated changes

Created src/number_theory/divisors.lean

added theorem nat.divisor_le

added def nat.divisors

added def nat.divisors_antidiagonal

added theorem nat.divisors_antidiagonal_one

added theorem nat.divisors_antidiagonal_zero

added theorem nat.divisors_eq_proper_divisors_insert_self

added theorem nat.divisors_zero

added theorem nat.fst_mem_divisors_of_mem_antidiagonal

added theorem nat.map_swap_divisors_antidiagonal

added theorem nat.mem_divisors

added theorem nat.mem_divisors_antidiagonal

added theorem nat.mem_proper_divisors

added def nat.perfect

added theorem nat.perfect_iff_sum_divisors_eq_two_mul

added theorem nat.perfect_iff_sum_proper_divisors

added theorem nat.proper_divisors.not_self_mem

added def nat.proper_divisors

added theorem nat.proper_divisors_zero

added theorem nat.snd_mem_divisors_of_mem_antidiagonal

added theorem nat.sum_divisors_eq_sum_proper_divisors_add_self

added theorem nat.swap_mem_divisors_antidiagonal