Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.prime.eq_of_factorization_pos

Modification history

2022-08-29 11:13

src/data/nat/factorization/basic.lean

feat(data/nat/factorization/basic): lemmas about `n.factorization p = 0` (#16185) …

Added nat.prime.eq_of_factorization_pos View on Github →