Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 ea88bd61

View on Github →

refactor(algebra/triv_sq_zero_ext): generalize and cleanup (#10729) This:

  • Generalizes typeclass assumptions on many lemmas
  • Generalizes and adds missing typeclass instances on triv_sq_zero_ext, most notably the algebra structure over a different ring.
  • Reorders many of the lemmas in the file to ensure that the right arguments are implicit / explicit

Estimated changes