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] : SMulCommClass S'ᵈᵐᵃ T'ᵈᵐᵃ (M →ₛₗ[σ₁₂] 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] : DistribMulAction S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.instDistribMulActionDomMulActOfSMulCommClass = DistribMulAction.mk ⋯ ⋯

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 ⋯ ⋯