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
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
