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