mathlib3
feat(data/nat/factorization/basic): lemmas about factorizations of sums and subtractions
#16231
Open
Open
feat(data/nat/factorization/basic): lemmas about factorizations of sums and subtractions #16231
stuart-presnell
wants to merge
36 commits into
master
from
SP_factorization_add_sub
Add drafts of three new lemmas
c79e32c3
Rename lemmas
5e11750c
Move lemma; add docstrings
09a8957b
Move and golf lemmas
8e65dbc9
Golf proofs
6f1afde7
Rename lemma
39b9d0b6
Move lemmas
bfc3a341
Fill in docstrings
8bfdc877
Add `prime.eq_of_factorization_pos`
5a92929e
Start `factorization_add_of_lt`
2604198e
Progress on `factorization_add_of_lt`
6eb8b0e0
Merge branch 'SP_factorization_eq_zero' into SP_factorization_add_sub
4d01737f
First proof of `factorization_add_of_lt`
c7a5ddfc
Remove `factorization_eq_zero_iff_remainder'`
719f05f5
Add `factorization_add_min`
5b26b202
Golf `factorization_add_of_lt`
111e6940
Further golf
e4b3ecdc
Add `factorization_sub_of_lt`
1ab6c757
Extract `factorization_eq_of_lt_factorization_add`
6b77b036
Add `factorization_add`
c7c14ae3
Add section docstring
616a26cb
`factorization_sub_of_lt'` & `factorization_sub_min`
b454d890
Change var in `factorization_eq_of_lt_factorization_add`
a6452149
Golf
ff25e39e
Add section docstring
f6ed1260
Remove unused args to fix lint error
b049100a
First proof of `factorization_sub`
f9406225
Golf
b5bfaf4d
Golf
c2557da6
Extract `factorization_add_le_of_factorization_add_eq`
ce239945
Start `factorization_add_iff`; golf `factorization_add_of_lt`
1510b706
Prove `factorization_add_iff`
ddc2d35f
Add docstrings
6312c024
Remove TODO
018f0e6a
Add lemma `factorization_sub_iff`
9f1a0c9c
Merge branch 'master' into SP_factorization_add_sub
8637c368
riccardobrasca
commented
on 2022-09-05
Reviewers
Assignees
No one assigned
Labels
awaiting-author
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub