mathlib

26690624 - feat(data/monoid_algebra): some lemmas about group rings (#2239)

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