Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 19:49 515ce797

View on Github →

refactor(data/nat/factorization): Use factorization instead of factors.count (#11384) Refactor to use factorization over factors.count, and adjust lemmas to be stated in terms of the former instead.

Estimated changes

added theorem nat.factorization_div
modified theorem nat.factorization_pow
modified theorem nat.factorization_zero
added theorem nat.factors_count_eq
modified theorem nat.pow_factorization_dvd
modified theorem nat.prime.factorization_pow
added def nat.rec_on_mul
modified theorem nat.support_factorization
deleted def nat.rec_on_mul
modified theorem nat.eq_of_perm_factors
deleted theorem nat.factors_count_pow
modified theorem nat.mem_factors_iff_dvd
modified theorem nat.mem_factors_mul_left
modified theorem nat.mem_factors_mul_right
added theorem nat.perm_factors_mul
deleted theorem nat.pow_factors_count_dvd
modified theorem nat.prod_factors