basic): two trivial simp lemmas about factorizations (#14634)

Commit

3 years ago

feat(data/nat/factorization/basic): two trivial simp lemmas about factorizations (#14634) For any `n : ℕ`, `n.factorization 0 = 0` and `n.factorization 1 = 0`

Author

stuart-presnell

Parents

4fc35392

mathlib3 b392bb2c - feat(data/nat/factorization/basic): two trivial simp lemmas about factorizations (#14634)

mathlib3
b392bb2c - feat(data/nat/factorization/basic): two trivial simp lemmas about factorizations (#14634)