mathlib documentation

algebra.module.algebra

Additional facts about modules over algebras. #

def linear_map.restrict_scalars_linear_map (k : Type u_1) [comm_semiring k] (A : Type u_2) [semiring A] [algebra k A] (M : Type u_3) [add_comm_monoid M] [module k M] [module A M] [is_scalar_tower k A M] (N : Type u_4) [add_comm_monoid N] [module k N] [module A N] [is_scalar_tower k A N] :

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

Equations
@[simp]
theorem linear_map.restrict_scalars_linear_map_apply (k : Type u_1) [comm_semiring k] (A : Type u_2) [semiring A] [algebra k A] (M : Type u_3) [add_comm_monoid M] [module k M] [module A M] [is_scalar_tower k A M] (N : Type u_4) [add_comm_monoid N] [module k N] [module A N] [is_scalar_tower k A N] (fₗ : M →ₗ[A] N) :