mathlib3
515ce797 - refactor(data/nat/factorization): Use factorization instead of factors.count (#11384)

Commit
3 years ago
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. Co-authored-by: Eric <ericrboidi@gmail.com> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com> Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com>
Author
Parents
Loading