mathlib
45d45ef0 - feat(data/nat/prime): lemma count_factors_mul_of_coprime (#10492)

Commit
4 years ago
feat(data/nat/prime): lemma count_factors_mul_of_coprime (#10492) Adding lemma `count_factors_mul_of_coprime` and using it to simplify the proof of `factors_count_eq_of_coprime_left`.
Parents
Loading