Commit 2020-03-31 11:30 26690624
View on Github →feat(data/monoid_algebra): some lemmas about group rings (#2239)
- feat(algebra/ring): generalize mul_ite
- fix proofs
- going off the deep-end
- cleaning up
- much better
- getting there
- no new congr lemma
- oops
- ...
- to_additive
- removing bad simp lemmas again...
- fix proof
- fix'
- oops
- feat(data/monoid_algebra): some lemmas about group rings
- Update src/algebra/ring.lean
- remove unnecessary arguments, thanks linter
- err.. marking simp again, because I can't remember what goes wrong and need CI to compile for me
- handing it back to CI for another try
- fix prod_ite as well
- cast_ite
- gross fix for quadratic reciprocity argument
- remove simp from add_ite, add comment
- sadness
- slight improvement
- remove redundant lemmas