PR #2223 feat(algebra/ring): generalize mul_ite

feat(algebra/ring): generalize mul_ite #2223

mergify merged 24 commits into master from mul_ite

feat(algebra/ring): generalize mul_ite

b5baa250

fix proofs

81156fa6

gebner commented on 2020-03-23

going off the deep-end

e51076ff

cleaning up

57c917f2

much better

1a860d5c

getting there

118bd297

no new congr lemma

aff97809

oops

9c900c9e

Merge remote-tracking branch 'origin/master' into mul_ite

ea97417e

...

c8d80d53

urkud commented on 2020-03-24

robertylewis added awaiting-author

to_additive

503d7c18

removing bad simp lemmas again...

8575a225

fix proof

85c8cec0

fix'

9c6b6f80

oops

75ef77d7

Merge remote-tracking branch 'origin/master' into mul_ite

84806f75

kim-em removed awaiting-author

kim-em added awaiting-review

kim-em commented on 2020-03-25

Update src/algebra/ring.lean

a326e67f

cipher1024 assigned

gebner 6 years ago

gebner commented on 2020-03-26

err.. marking simp again, because I can't remember what goes wrong an…

fb3ae405

handing it back to CI for another try

b8c7f28d

fix prod_ite as well

2c31f6f5

cast_ite

5b39eccc

kim-em removed awaiting-review

kim-em added awaiting-author

gross fix for quadratic reciprocity argument

ba3883a6

remove simp from add_ite, add comment

b5ab0024

gebner added ready-to-merge

gebner removed awaiting-author

gebner approved these changes on 2020-03-27

Merge branch 'master' into mul_ite

3ebb7326

mergify merged d0a85073 into master 6 years ago

bryangingechen deleted the mul_ite branch 6 years ago

Reviewers

gebner

urkud

Assignees

gebner

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(algebra/ring): generalize mul_ite #2223 Merged

feat(algebra/ring): generalize mul_ite #2223

mathlib3
feat(algebra/ring): generalize mul_ite
#2223

Merged