Commit 2022-12-08 18:41 10b4e499

View on Github →

chore(data/nat/prime): reduce imports more (#17854) This relocates the norm_num plugin and nat.factors, and rewrites a proof without wlog, to avoid depending on a reasonably sized chunk of results about lists.

Estimated changes

Modified archive/100-theorems-list/16_abel_ruffini.lean

Modified archive/imo/imo1988_q6.lean

Modified archive/imo/imo2005_q4.lean

Created src/data/nat/factors.lean

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.factors_pow

added theorem nat.prime_of_mem_factors

added theorem nat.prod_factors

Modified src/data/nat/parity.lean

Modified src/data/nat/prime.lean

deleted theorem nat.coprime_factors_disjoint

deleted theorem nat.dvd_of_factors_subperm

deleted theorem nat.dvd_of_mem_factors

deleted theorem nat.eq_of_perm_factors

deleted theorem nat.eq_prime_pow_of_unique_prime_dvd

deleted theorem nat.eq_two_pow_or_exists_odd_prime_and_dvd

deleted def nat.factors

deleted theorem nat.factors_add_two

deleted theorem nat.factors_chain'

deleted theorem nat.factors_chain

deleted theorem nat.factors_chain_2

deleted theorem nat.factors_eq_nil

deleted theorem nat.factors_one

deleted theorem nat.factors_prime

deleted theorem nat.factors_sorted

deleted theorem nat.factors_sublist_of_dvd

deleted theorem nat.factors_sublist_right

deleted theorem nat.factors_subset_of_dvd

deleted theorem nat.factors_subset_right

deleted theorem nat.factors_unique

deleted theorem nat.factors_zero

deleted theorem nat.le_of_mem_factors

deleted theorem nat.mem_factors

deleted theorem nat.mem_factors_iff_dvd

deleted theorem nat.mem_factors_mul

deleted theorem nat.mem_factors_mul_left

deleted theorem nat.mem_factors_mul_of_coprime

deleted theorem nat.mem_factors_mul_right

deleted theorem nat.perm_factors_mul

deleted theorem nat.perm_factors_mul_of_coprime

deleted theorem nat.pos_of_mem_factors

deleted theorem nat.prime.factors_pow

deleted theorem nat.prime_of_mem_factors

modified theorem nat.prime_three

deleted theorem nat.prod_factors

deleted def tactic.norm_num.factors_helper

deleted theorem tactic.norm_num.factors_helper_cons'

deleted theorem tactic.norm_num.factors_helper_cons

deleted theorem tactic.norm_num.factors_helper_end

deleted theorem tactic.norm_num.factors_helper_nil

deleted theorem tactic.norm_num.factors_helper_same

deleted theorem tactic.norm_num.factors_helper_same_sn

deleted theorem tactic.norm_num.factors_helper_sn

deleted theorem tactic.norm_num.is_prime_helper

deleted theorem tactic.norm_num.min_fac_bit0

deleted theorem tactic.norm_num.min_fac_helper.n_pos

deleted def tactic.norm_num.min_fac_helper

deleted theorem tactic.norm_num.min_fac_helper_0

deleted theorem tactic.norm_num.min_fac_helper_1

deleted theorem tactic.norm_num.min_fac_helper_2

deleted theorem tactic.norm_num.min_fac_helper_3

deleted theorem tactic.norm_num.min_fac_helper_4

deleted theorem tactic.norm_num.min_fac_helper_5

deleted theorem tactic.norm_num.min_fac_ne_bit0

Modified src/data/nat/prime_fin.lean

Created src/data/nat/prime_norm_num.lean

added def tactic.norm_num.factors_helper

added theorem tactic.norm_num.factors_helper_cons'

added theorem tactic.norm_num.factors_helper_cons

added theorem tactic.norm_num.factors_helper_end

added theorem tactic.norm_num.factors_helper_nil

added theorem tactic.norm_num.factors_helper_same

added theorem tactic.norm_num.factors_helper_same_sn

added theorem tactic.norm_num.factors_helper_sn

added theorem tactic.norm_num.is_prime_helper

added theorem tactic.norm_num.min_fac_bit0

added theorem tactic.norm_num.min_fac_helper.n_pos

added def tactic.norm_num.min_fac_helper

added theorem tactic.norm_num.min_fac_helper_0

added theorem tactic.norm_num.min_fac_helper_1

added theorem tactic.norm_num.min_fac_helper_2

added theorem tactic.norm_num.min_fac_helper_3

added theorem tactic.norm_num.min_fac_helper_4

added theorem tactic.norm_num.min_fac_helper_5

added theorem tactic.norm_num.min_fac_ne_bit0

Modified src/data/nat/squarefree.lean

Modified src/data/pnat/factors.lean

Modified src/data/real/golden_ratio.lean

Modified src/number_theory/bertrand.lean

Modified src/number_theory/divisors.lean

Modified src/number_theory/fermat4.lean

Modified src/number_theory/lucas_lehmer.lean

Modified src/ring_theory/int/basic.lean