Commit 2023-01-29 02:08 38f7548b

View on Github →

feat: port NumberTheory.Divisors (#1912)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Divisors.lean

added def Nat.Perfect

added theorem Nat.Prime.divisors

added theorem Nat.Prime.prod_divisors

added theorem Nat.Prime.prod_properDivisors

added theorem Nat.Prime.properDivisors

added theorem Nat.cons_self_properDivisors

added theorem Nat.divisor_le

added def Nat.divisors

added def Nat.divisorsAntidiagonal

added theorem Nat.divisorsAntidiagonal_one

added theorem Nat.divisorsAntidiagonal_zero

added theorem Nat.divisors_one

added theorem Nat.divisors_prime_pow

added theorem Nat.divisors_subset_of_dvd

added theorem Nat.divisors_subset_properDivisors

added theorem Nat.divisors_zero

added theorem Nat.dvd_of_mem_divisors

added theorem Nat.eq_properDivisors_of_subset_of_sum_eq_sum

added theorem Nat.filter_dvd_eq_divisors

added theorem Nat.filter_dvd_eq_properDivisors

added theorem Nat.fst_mem_divisors_of_mem_antidiagonal

added theorem Nat.image_div_divisors_eq_divisors

added theorem Nat.image_fst_divisorsAntidiagonal

added theorem Nat.image_snd_divisorsAntidiagonal

added theorem Nat.insert_self_properDivisors

added theorem Nat.map_div_left_divisors

added theorem Nat.map_div_right_divisors

added theorem Nat.map_swap_divisorsAntidiagonal

added theorem Nat.mem_divisors

added theorem Nat.mem_divisorsAntidiagonal

added theorem Nat.mem_divisors_prime_pow

added theorem Nat.mem_divisors_self

added theorem Nat.mem_properDivisors

added theorem Nat.mem_properDivisors_prime_pow

added theorem Nat.one_mem_divisors

added theorem Nat.one_mem_properDivisors_iff_one_lt

added theorem Nat.perfect_iff_sum_divisors_eq_two_mul

added theorem Nat.perfect_iff_sum_properDivisors

added theorem Nat.pos_of_mem_divisors

added theorem Nat.pos_of_mem_properDivisors

added theorem Nat.prime_divisors_eq_to_filter_divisors_prime

added theorem Nat.prod_div_divisors

added theorem Nat.prod_divisorsAntidiagonal'

added theorem Nat.prod_divisorsAntidiagonal

added theorem Nat.prod_divisors_prime_pow

added theorem Nat.prod_properDivisors_prime_pow

added theorem Nat.properDivisors.not_self_mem

added def Nat.properDivisors

added theorem Nat.properDivisors_eq_singleton_one_iff_prime

added theorem Nat.properDivisors_one

added theorem Nat.properDivisors_prime_pow

added theorem Nat.properDivisors_subset_divisors

added theorem Nat.properDivisors_zero

added theorem Nat.snd_mem_divisors_of_mem_antidiagonal

added theorem Nat.sum_divisors_eq_sum_properDivisors_add_self

added theorem Nat.sum_properDivisors_dvd

added theorem Nat.sum_properDivisors_eq_one_iff_prime

added theorem Nat.swap_mem_divisorsAntidiagonal

added theorem Nat.swap_mem_divisorsAntidiagonal_aux