Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added theorem ite_pow
added theorem pow_boole
added theorem pow_ite
added theorem boole_mul
modified theorem ite_mul
added theorem mul_boole
modified theorem mul_ite