Commit 2021-07-13 15:34 815e91f3

View on Github →

chore(data/nat/prime): fix + add missing lemmas (#8066) I fixed up some indents as well, as they were bothering me quite a bit. The only "new" content is 597 - 617.

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.factors_subset_of_dvd

added theorem nat.factors_subset_right

modified theorem nat.le_min_fac'

modified theorem nat.le_min_fac

modified def nat.min_fac

modified def nat.min_fac_aux

modified theorem nat.min_fac_aux_has_prop

modified theorem nat.min_fac_dvd

modified theorem nat.min_fac_eq

modified theorem nat.min_fac_eq_one_iff

modified theorem nat.min_fac_eq_two_iff

modified theorem nat.min_fac_has_prop

modified theorem nat.min_fac_le

modified theorem nat.min_fac_le_div

modified theorem nat.min_fac_le_of_dvd

modified theorem nat.min_fac_one

modified theorem nat.min_fac_pos

modified theorem nat.min_fac_prime

modified theorem nat.min_fac_sq_le_self

modified theorem nat.min_fac_zero

modified theorem nat.not_prime_iff_min_fac_lt

modified theorem nat.prime_def_min_fac