Commit 2021-11-23 21:34 ac283c22

View on Github →

feat(data/nat/prime): some lemmas about prime factors (#10385) A few small lemmas about prime factors, for use in future PRs on prime factorisations and the Euler product formula for totient

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.factors_count_eq_of_coprime_left

added theorem nat.factors_count_eq_of_coprime_right

added theorem nat.le_factors_count_mul_left

added theorem nat.le_factors_count_mul_right

added theorem nat.mem_factors_mul_left

added theorem nat.mem_factors_mul_right

added theorem nat.perm_factors_mul_of_coprime

added theorem nat.perm_factors_mul_of_pos