Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-05 00:35 efa4f92e

View on Github →

feat(data/nat/prime): lemmas about nat.factors

Estimated changes

Modified data/nat/prime.lean

added theorem nat.factors_unique

added theorem nat.mem_factors

added theorem nat.mem_factors_of_dvd

added theorem nat.mem_list_primes_of_dvd_prod

added theorem nat.perm_of_prod_eq_prod

added theorem nat.prod_factors