# mathlibdocumentation

algebra.module.algebra

Restriction of scalars for linear maps between modules over a k-algebra is itself k-linear.