Commit 2020-11-17 17:53 e92b5acd

feat(algebra/opposites): Provide semimodule instances and op_linear_equiv (#4954) We already have a has_scalar definition via an algebra definition. The definition used there satisfies a handful of other typeclasses too, and also allows for op_add_equiv to be stated more strongly as op_linear_equiv. This also cuts back the imports a little on algebra.module.basic, which means formerly-transitive imports have to be added to downstream files.