Commit 2022-02-20 09:43 6c6e142e

View on Github →

chore(data/nat/factorization): Reorder lemmas and some minor golfing (#12144) Some minor housework on this file, reordering and regrouping lemmas, adding and editing a few docstrings and section headers, and golfing a few proofs.

Estimated changes

Modified src/data/nat/factorization.lean

modified theorem nat.pos_of_mem_factorization

modified theorem nat.prime_of_mem_factorization

deleted def nat.rec_on_pos_prime_coprime

added def nat.rec_on_pos_prime_pos_coprime