mathlib3
feat(algebra/ring): generalize mul_ite
#2223
Merged
Overview
Commits
24
Changes
View On GitHub
Commits
  • feat(algebra/ring): generalize mul_ite
    kim-em committed 6 years ago
  • fix proofs
    kim-em committed 6 years ago
  • going off the deep-end
    kim-em committed 6 years ago
  • cleaning up
    kim-em committed 6 years ago
  • much better
    kim-em committed 6 years ago
  • getting there
    kim-em committed 6 years ago
  • no new congr lemma
    kim-em committed 6 years ago
  • oops
    kim-em committed 6 years ago
  • Merge remote-tracking branch 'origin/master' into mul_ite
    kim-em committed 6 years ago
  • ...
    kim-em committed 6 years ago
  • to_additive
    kim-em committed 6 years ago
  • removing bad simp lemmas again...
    kim-em committed 6 years ago
  • fix proof
    kim-em committed 6 years ago
  • fix'
    kim-em committed 6 years ago
  • oops
    kim-em committed 6 years ago
  • Merge remote-tracking branch 'origin/master' into mul_ite
    kim-em committed 6 years ago
  • Update src/algebra/ring.lean
    kim-em committed 6 years ago
  • err.. marking simp again, because I can't remember what goes wrong and need CI to compile for me
    kim-em committed 6 years ago
  • handing it back to CI for another try
    kim-em committed 6 years ago
  • fix prod_ite as well
    kim-em committed 6 years ago
  • cast_ite
    kim-em committed 6 years ago
  • gross fix for quadratic reciprocity argument
    kim-em committed 6 years ago
  • remove simp from add_ite, add comment
    kim-em committed 6 years ago
  • Merge branch 'master' into mul_ite
    mergify[bot] committed 6 years ago
FAQ Terms Privacy Refunds Impressum
Loading