Commit 2022-01-23 15:43 5449ffa4

View on Github →

feat(data/nat/prime): factors of non-prime powers (#11546) Adds the result pow_factors_to_finset, fills in factors_mul_to_finset_of_coprime for the sake of completion, and adjusts statements to take ne_zero rather than pos assumptions.

Estimated changes

Modified src/data/finset/basic.lean

added theorem list.to_finset.ext

added theorem list.to_finset.ext_iff

Modified src/data/nat/factorization.lean

added theorem nat.factorization_mul_support

deleted theorem nat.factorization_mul_support_of_pos

Modified src/data/nat/prime.lean

modified theorem nat.coprime_factors_disjoint

deleted theorem nat.factors_mul_of_coprime

deleted theorem nat.factors_mul_of_pos

added theorem nat.factors_mul_to_finset

added theorem nat.factors_mul_to_finset_of_coprime

modified theorem nat.mem_factors

added theorem nat.mem_factors_mul

added theorem nat.mem_factors_mul_of_coprime

deleted theorem nat.mem_factors_mul_of_pos

added theorem nat.pow_factors_to_finset

added theorem nat.pow_succ_factors_to_finset

modified theorem nat.prime_pow_prime_divisor

Modified src/group_theory/p_group.lean