Further results on (semi)linear maps

def LinearMap.ltoFun (R : Type u_6) (M : Type u_7) (N : Type u_8) (A : Type u_9) [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [SMulCommClass R A N] : (M →ₗ[R] N) →ₗ[A] M → N

A-linearly coerce an R-linear map from M to N to a function, when N has commuting R-module and A-module structures.

@[simp]

theorem LinearMap.ltoFun_apply {R : Type u_6} {M : Type u_7} {N : Type u_8} {A : Type u_9} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module A N] [SMulCommClass R A N] {f : M →ₗ[R] N} : (ltoFun R M N A) f = ⇑f

@[implicit_reducible]

instance LinearMap.instSMulDomMulAct {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] : SMul S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')

theorem DomMulAct.smul_linearMap_apply {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') (x : M) : (a • f) x = f (mk.symm a • x)

@[simp]

theorem DomMulAct.mk_smul_linearMap_apply {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S') (f : M →ₛₗ[σ₁₂] M') (x : M) : (mk a • f) x = f (a • x)

theorem DomMulAct.coe_smul_linearMap {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [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_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} {T' : Type u_7} [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')

@[implicit_reducible]

instance LinearMap.instDistribMulActionDomMulActOfSMulCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} {S' : Type u_6} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] : DistribMulAction S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')

instance LinearMap.instIsTorsionFree {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [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.IsTorsionFree S M'] : Module.IsTorsionFree S (M →ₛₗ[σ₁₂] M')

@[implicit_reducible]

instance LinearMap.instModuleDomMulActOfSMulCommClass {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [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')

@[simp]

theorem LinearMap.mulLeft_mul (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] (a b : A) : mulLeft R (a * b) = mulLeft R a ∘ₗ mulLeft R b

@[simp]

theorem LinearMap.mulRight_mul (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) : mulRight R (a * b) = mulRight R b ∘ₗ mulRight R a

@[simp]

theorem LinearMap.mulLeft_inj {R : Type u_6} {A : Type u_7} [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] {a b : A} : mulLeft R a = mulLeft R b ↔ a = b

@[simp]

theorem LinearMap.mulRight_inj {R : Type u_6} {A : Type u_7} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] {a b : A} : mulRight R a = mulRight R b ↔ a = b

@[simp]

theorem LinearMap.mulLeft_one (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] : mulLeft R 1 = id

@[simp]

theorem LinearMap.mulLeft_eq_zero_iff (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [SMulCommClass R A A] (a : A) : mulLeft R a = 0 ↔ a = 0

@[simp]

theorem LinearMap.mulRight_one (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] : mulRight R 1 = id

@[simp]

theorem LinearMap.mulRight_eq_zero_iff (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a : A) : mulRight R a = 0 ↔ a = 0

def Sum.elimZeroLeft {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] : (ι → R) →ₗ[R] κ ⊕ ι → R

The map Sum.elim specialised with zero in the first argument, as a linear map.

@[simp]

theorem Sum.elimZeroLeft_apply {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] (g : ι → R) (a✝ : κ ⊕ ι) : elimZeroLeft g a✝ = Sum.elim 0 g a✝

def Sum.elimZeroRight {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] : (ι → R) →ₗ[R] ι ⊕ κ → R

The map Sum.elim specialised with zero in the second argument, as a linear map.

@[simp]

theorem Sum.elimZeroRight_apply {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [Semiring R] (f : ι → R) (a✝ : ι ⊕ κ) : elimZeroRight f a✝ = Sum.elim f 0 a✝