Commit 2020-03-27 21:37 d0a85073
View on Github →feat(algebra/ring): generalize mul_ite (#2223)
- 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
- Update src/algebra/ring.lean
- 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