Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 15:18 7ab3af8f

View on Github →

chore(data.nat.prime): reduce imports (#17840)

Estimated changes

Modified archive/imo/imo1998_q2.lean

Modified src/algebra/associated.lean

deleted theorem associates.is_atom_iff

Modified src/algebra/gcd_monoid/multiset.lean

Modified src/algebra/punit_instances.lean

Modified src/data/nat/factorization/basic.lean

Modified src/data/nat/prime.lean

deleted theorem nat.factors_mul_to_finset

deleted theorem nat.factors_mul_to_finset_of_coprime

deleted theorem nat.infinite_set_of_prime

deleted theorem nat.pow_factors_to_finset

deleted theorem nat.pow_succ_factors_to_finset

deleted theorem nat.prime_pow_prime_divisor

Created src/data/nat/prime_fin.lean

added theorem nat.factors_mul_to_finset

added theorem nat.factors_mul_to_finset_of_coprime

added theorem nat.infinite_set_of_prime

added theorem nat.pow_factors_to_finset

added theorem nat.pow_succ_factors_to_finset

added theorem nat.prime_pow_prime_divisor

Modified src/data/pnat/factors.lean

Modified src/number_theory/prime_counting.lean

Modified src/number_theory/primes_congruent_one.lean

Modified src/ring_theory/chain_of_divisors.lean

added theorem associates.is_atom_iff