Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes