Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-22 19:46 2f5af98b

View on Github →

feat(data/nat/prime): prime divisors (#10318) Adding some basic lemmas about factors and factors.to_finset

Estimated changes

Modified src/data/finset/basic.lean

added theorem list.to_finset_repeat_of_ne_zero

Modified src/data/nat/gcd.lean

added theorem nat.eq_one_of_dvd_coprimes

Modified src/data/nat/prime.lean

added theorem nat.coprime_factors_disjoint

added theorem nat.dvd_of_mem_factors

added theorem nat.factors_mul_of_coprime

added theorem nat.factors_mul_of_pos

added theorem nat.mem_factors_mul_of_pos

added theorem nat.prime_pow_prime_divisor

Modified src/number_theory/divisors.lean

added theorem nat.prime_divisors_eq_to_filter_divisors_prime