Documentation

Mathlib.Algebra.Module.Algebra

Additional facts about modules over algebras. #

@[simp]
theorem LinearMap.restrictScalarsLinearMap_apply (k : Type u_1) [CommSemiring k] (A : Type u_2) [Semiring A] [Algebra k A] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (N : Type u_4) [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] (fₗ : M →ₗ[A] N) :
↑(LinearMap.restrictScalarsLinearMap k A M N) fₗ = k fₗ
def LinearMap.restrictScalarsLinearMap (k : Type u_1) [CommSemiring k] (A : Type u_2) [Semiring A] [Algebra k A] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (N : Type u_4) [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] :

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For