Additional typeclass for modules over an algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For an object in
M : Module A, where
A is a
we provide additional typeclasses on the underlying type
module k M and
is_scalar_tower k A M.
These are not made into instances by default.
We provide the
linear k (Module A) instance.
It seems without making a parallel version
Module' k A, for modules over a
that carries these typeclasses, this seems hard to achieve.
(An alternative would be to always require these typeclasses, and remove the original
requiring users to write
Module' ℤ A when
A is merely a ring.)