Commit 2023-03-28 12:18 8e91a9b4

View on Github →

feat: Port/Data.Nat.Factorization.Basic (#3043)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Factorization/Basic.lean

added theorem Nat.Icc_factorization_eq_pow_dvd

added theorem Nat.Ico_filter_pow_dvd_eq

added theorem Nat.Ioc_filter_dvd_card_eq_div

added theorem Nat.Prime.dvd_iff_one_le_factorization

added theorem Nat.Prime.eq_of_factorization_pos

added theorem Nat.Prime.factorization

added theorem Nat.Prime.factorization_pos_of_dvd

added theorem Nat.Prime.factorization_pow

added theorem Nat.Prime.factorization_self

added theorem Nat.Prime.pow_dvd_iff_dvd_ord_proj

added theorem Nat.Prime.pow_dvd_iff_le_factorization

added theorem Nat.card_multiples

added theorem Nat.coprime_ord_compl

added theorem Nat.dvd_iff_div_factorization_eq_tsub

added theorem Nat.dvd_iff_prime_pow_dvd_dvd

added theorem Nat.dvd_of_factorization_pos

added theorem Nat.dvd_of_mem_factorization

added theorem Nat.dvd_ord_compl_of_dvd_not_dvd

added theorem Nat.dvd_ord_proj_of_dvd

added theorem Nat.eq_factorization_iff

added theorem Nat.eq_iff_prime_padicValNat_eq

added theorem Nat.eq_of_factorization_eq

added theorem Nat.eq_pow_of_factorization_eq_single

added theorem Nat.exists_eq_pow_mul_and_not_dvd

added theorem Nat.exists_factorization_lt_of_lt

added theorem Nat.factor_iff_mem_factorization

added def Nat.factorization

added def Nat.factorizationEquiv

added theorem Nat.factorizationEquiv_apply

added theorem Nat.factorizationEquiv_inv_apply

added theorem Nat.factorization_def

added theorem Nat.factorization_disjoint_of_coprime

added theorem Nat.factorization_div

added theorem Nat.factorization_eq_card_pow_dvd

added theorem Nat.factorization_eq_factors_multiset

added theorem Nat.factorization_eq_of_coprime_left

added theorem Nat.factorization_eq_of_coprime_right

added theorem Nat.factorization_eq_zero_iff'

added theorem Nat.factorization_eq_zero_iff

added theorem Nat.factorization_eq_zero_iff_remainder

added theorem Nat.factorization_eq_zero_of_lt

added theorem Nat.factorization_eq_zero_of_non_prime

added theorem Nat.factorization_eq_zero_of_not_dvd

added theorem Nat.factorization_eq_zero_of_remainder

added theorem Nat.factorization_gcd

added theorem Nat.factorization_inj

added theorem Nat.factorization_lcm

added theorem Nat.factorization_le_factorization_mul_left

added theorem Nat.factorization_le_factorization_mul_right

added theorem Nat.factorization_le_iff_dvd

added theorem Nat.factorization_le_of_le_pow

added theorem Nat.factorization_lt

added theorem Nat.factorization_mul

added theorem Nat.factorization_mul_apply_of_coprime

added theorem Nat.factorization_mul_of_coprime

added theorem Nat.factorization_mul_support

added theorem Nat.factorization_mul_support_of_coprime

added theorem Nat.factorization_one

added theorem Nat.factorization_one_right

added theorem Nat.factorization_ord_compl

added theorem Nat.factorization_pow

added theorem Nat.factorization_prime_le_iff_dvd

added theorem Nat.factorization_prod

added theorem Nat.factorization_prod_pow_eq_self

added theorem Nat.factorization_zero

added theorem Nat.factorization_zero_right

added theorem Nat.factors_count_eq

added theorem Nat.le_of_mem_factorization

added theorem Nat.multiplicative_factorization'

added theorem Nat.multiplicative_factorization

added theorem Nat.multiplicity_eq_factorization

added theorem Nat.not_dvd_ord_compl

added theorem Nat.ord_compl_dvd

added theorem Nat.ord_compl_dvd_ord_compl_iff_dvd

added theorem Nat.ord_compl_dvd_ord_compl_of_dvd

added theorem Nat.ord_compl_le

added theorem Nat.ord_compl_mul

added theorem Nat.ord_compl_of_not_prime

added theorem Nat.ord_compl_pos

added theorem Nat.ord_proj_dvd

added theorem Nat.ord_proj_dvd_ord_proj_iff_dvd

added theorem Nat.ord_proj_dvd_ord_proj_of_dvd

added theorem Nat.ord_proj_le

added theorem Nat.ord_proj_mul

added theorem Nat.ord_proj_mul_ord_compl_eq_self

added theorem Nat.ord_proj_of_not_prime

added theorem Nat.ord_proj_pos

added theorem Nat.pos_of_mem_factorization

added theorem Nat.pow_succ_factorization_not_dvd

added theorem Nat.prime_of_mem_factorization

added theorem Nat.prod_factorization_eq_prod_factors

added theorem Nat.prod_factors_gcd_mul_prod_factors_mul

added theorem Nat.prod_pow_factorization_eq_self

added theorem Nat.prod_pow_prime_padicValNat

added theorem Nat.prod_prime_factors_dvd

added def Nat.recOnPosPrimePosCoprime

added def Nat.recOnPrimeCoprime

added def Nat.recOnPrimePow

added theorem Nat.setOf_pow_dvd_eq_Icc_factorization

added theorem Nat.support_factorization