feat(data/monoid_algebra): some lemmas about group rings #2239
mergify
merged
35 commits into
master
from
group_ring_lemmas
feat(algebra/ring): generalize mul_ite
b5baa250
fix proofs
81156fa6
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
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
feat(data/monoid_algebra): some lemmas about group rings
fbd9eab4
Update src/algebra/ring.lean
a326e67f
remove unnecessary arguments, thanks linter
24d02946
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
gross fix for quadratic reciprocity argument
ba3883a6
remove simp from add_ite, add comment
b5ab0024
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into mul_ite
3ebb7326
Merge branch 'mul_ite' into group_ring_lemmas
347c54cb
kim-em
changed the title
sadness
3187927c
slight improvement
9b74291b
Merge remote-tracking branch 'origin/master' into group_ring_lemmas
631e74e4
remove redundant lemmas
7ff5a66f
ChrisHughes24
approved these changes
on 2020-03-30
Merge branch 'master' into group_ring_lemmas
52dfdeee
Merge remote-tracking branch 'origin/master' into HEAD
586b13cb
Merge branch 'master' into group_ring_lemmas
9f6485b9
Merge branch 'master' into group_ring_lemmas
9f9ecbeb
Login to write a write a comment.
Login via GitHub