Documentation

Mathlib.Algebra.Module.LinearMap.Basic

Further results on (semi)linear maps #

instance LinearMap.instSMulDomMulAct {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :
SMul S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M₂)
Equations
  • LinearMap.instSMulDomMulAct = { smul := fun (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) => { toFun := a f, map_add' := , map_smul' := } }
theorem DomMulAct.smul_linearMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
(a f) x = f (DomMulAct.mk.symm a x)
@[simp]
theorem DomMulAct.mk_smul_linearMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S') (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
(DomMulAct.mk a f) x = f (a x)
theorem DomMulAct.coe_smul_linearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) :
(a f) = a f
instance LinearMap.instSMulCommClassDomMulAct {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} {T' : Type u_18} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] [Monoid T'] [DistribMulAction T' M] [SMulCommClass R T' M] [SMulCommClass S' T' M] :
Equations
  • =
instance LinearMap.instDistribMulActionDomMulActOfSMulCommClass {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :
Equations
instance LinearMap.instNoZeroSMulDivisors {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] [NoZeroSMulDivisors S M₂] :
NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)
Equations
  • =
instance LinearMap.instModuleDomMulActOfSMulCommClass {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M] [SMulCommClass R S M] :
Module Sᵈᵐᵃ (M →ₛₗ[σ₁₂] M₂)
Equations
  • LinearMap.instModuleDomMulActOfSMulCommClass = Module.mk