Commit 2023-01-20 09:59 346d9bc7

View on Github →

feat: port Data.Nat.Factors (#1664)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Factors.lean

added theorem Nat.Prime.factors_pow

added theorem Nat.coprime_factors_disjoint

added theorem Nat.dvd_of_factors_subperm

added theorem Nat.dvd_of_mem_factors

added theorem Nat.eq_of_perm_factors

added theorem Nat.eq_prime_pow_of_unique_prime_dvd

added theorem Nat.eq_two_pow_or_exists_odd_prime_and_dvd

added def Nat.factors

added theorem Nat.factors_add_two

added theorem Nat.factors_chain'

added theorem Nat.factors_chain

added theorem Nat.factors_chain_2

added theorem Nat.factors_eq_nil

added theorem Nat.factors_one

added theorem Nat.factors_prime

added theorem Nat.factors_sorted

added theorem Nat.factors_sublist_of_dvd

added theorem Nat.factors_sublist_right

added theorem Nat.factors_subset_of_dvd

added theorem Nat.factors_subset_right

added theorem Nat.factors_unique

added theorem Nat.factors_zero

added theorem Nat.le_of_mem_factors

added theorem Nat.mem_factors

added theorem Nat.mem_factors_iff_dvd

added theorem Nat.mem_factors_mul

added theorem Nat.mem_factors_mul_left

added theorem Nat.mem_factors_mul_of_coprime

added theorem Nat.mem_factors_mul_right

added theorem Nat.perm_factors_mul

added theorem Nat.perm_factors_mul_of_coprime

added theorem Nat.pos_of_mem_factors

added theorem Nat.prime_of_mem_factors

added theorem Nat.prod_factors