mathlib
ea88bd61 - refactor(algebra/triv_sq_zero_ext): generalize and cleanup (#10729)

Commit
4 years ago
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
Author
Parents
Loading