# Theory of topological modules and continuous linear maps. #

We use the class ContinuousSMul for topological (semi) modules and topological vector spaces.

In this file we define continuous (semi-)linear maps, as semilinear maps between topological modules which are continuous. The set of continuous semilinear maps between the topological R₁-module M and R₂-module M₂ with respect to the RingHom σ is denoted by M →SL[σ] M₂. Plain linear maps are denoted by M →L[R] M₂ and star-linear maps by M →L⋆[R] M₂.

The corresponding notation for equivalences is M ≃SL[σ] M₂, M ≃L[R] M₂ and M ≃L⋆[R] M₂.

theorem ContinuousSMul.of_nhds_zero {R : Type u_1} {M : Type u_2} [Ring R] [] [] [] [Module R M] [] (hmul : Filter.Tendsto (fun (p : R × M) => p.1 p.2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmulleft : ∀ (m : M), Filter.Tendsto (fun (a : R) => a m) (nhds 0) (nhds 0)) (hmulright : ∀ (a : R), Filter.Tendsto (fun (m : M) => a m) (nhds 0) (nhds 0)) :
theorem Submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [Ring R] [] [] [] [] [Module R M] [] [(nhdsWithin 0 {x : R | }).NeBot] (s : ) (hs : (interior s).Nonempty) :
s =

If M is a topological module over R and 0 is a limit of invertible elements of R, then ⊤ is the only submodule of M with a nonempty interior. This is the case, e.g., if R is a nontrivially normed field.

theorem Module.punctured_nhds_neBot (R : Type u_1) (M : Type u_2) [Ring R] [] [] [] [] [Module R M] [] [] [(nhdsWithin 0 {0}).NeBot] [] (x : M) :
(nhdsWithin x {x}).NeBot

Let R be a topological ring such that zero is not an isolated point (e.g., a nontrivially normed field, see NormedField.punctured_nhds_neBot). Let M be a nontrivial module over R such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this using NeBot (𝓝[≠] x).

This lemma is not an instance because Lean would need to find [ContinuousSMul ?m_1 M] with unknown ?m_1. We register this as an instance for R = ℝ in Real.punctured_nhds_module_neBot. One can also use haveI := Module.punctured_nhds_neBot R M in a proof.

theorem continuousSMul_induced {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [Module R M₁] [Module R M₂] [u : ] {t : } [] (f : M₁ →ₗ[R] M₂) :
theorem TopologicalSpace.IsSeparable.span {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] [] [] [] {s : Set M} (hs : ) :

The span of a separable subset with respect to a separable scalar ring is again separable.

instance Submodule.topologicalAddGroup {α : Type u_1} {β : Type u_2} [] [Ring α] [] [Module α β] (S : ) :
Equations
• =
theorem Submodule.mapsTo_smul_closure {R : Type u} {M : Type v} [] [] [] [Module R M] [] (s : ) (c : R) :
Set.MapsTo (fun (x : M) => c x) (closure s) (closure s)
theorem Submodule.smul_closure_subset {R : Type u} {M : Type v} [] [] [] [Module R M] [] (s : ) (c : R) :
c closure s closure s
def Submodule.topologicalClosure {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : ) :

The (topological-space) closure of a submodule of a topological R-module M is itself a submodule.

Equations
• s.topologicalClosure = let __src := s.topologicalClosure; { toAddSubmonoid := __src, smul_mem' := }
Instances For
@[simp]
theorem Submodule.topologicalClosure_coe {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : ) :
s.topologicalClosure = closure s
theorem Submodule.le_topologicalClosure {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : ) :
s s.topologicalClosure
theorem Submodule.closure_subset_topologicalClosure_span {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : Set M) :
(Submodule.span R s).topologicalClosure
theorem Submodule.isClosed_topologicalClosure {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : ) :
IsClosed s.topologicalClosure
theorem Submodule.topologicalClosure_minimal {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
theorem Submodule.topologicalClosure_mono {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] {s : } {t : } (h : s t) :
s.topologicalClosure t.topologicalClosure
theorem IsClosed.submodule_topologicalClosure_eq {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] {s : } (hs : IsClosed s) :
s.topologicalClosure = s

The topological closure of a closed submodule s is equal to s.

theorem Submodule.dense_iff_topologicalClosure_eq_top {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] {s : } :
Dense s s.topologicalClosure =

A subspace is dense iff its topological closure is the entire space.

instance Submodule.topologicalClosure.completeSpace {R : Type u} [] {M' : Type u_1} [] [Module R M'] [] [] [] [] (U : Submodule R M') :
CompleteSpace U.topologicalClosure
Equations
• =
theorem Submodule.isClosed_or_dense_of_isCoatom {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (s : ) (hs : ) :
IsClosed s Dense s

A maximal proper subspace of a topological module (i.e a Submodule satisfying IsCoatom) is either closed or dense.

theorem LinearMap.continuous_on_pi {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [] [] (f : (ιR) →ₗ[R] M) :
structure ContinuousLinearMap {R : Type u_1} {S : Type u_2} [] [] (σ : R →+* S) (M : Type u_3) [] [] (M₂ : Type u_4) [] [] [Module R M] [Module S M₂] extends :
Type (max u_3 u_4)

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

• toFun : MM₂
• map_add' : ∀ (x y : M), (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
• map_smul' : ∀ (m : R) (x : M), (↑self).toFun (m x) = σ m (↑self).toFun x
• cont : Continuous (↑self).toFun

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Instances For
theorem ContinuousLinearMap.cont {R : Type u_1} {S : Type u_2} [] [] {σ : R →+* S} {M : Type u_3} [] [] {M₂ : Type u_4} [] [] [Module R M] [Module S M₂] (self : M →SL[σ] M₂) :
Continuous (↑self).toFun

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

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

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class ContinuousSemilinearMapClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [] [] (σ : outParam (R →+* S)) (M : outParam (Type u_4)) [] [] (M₂ : outParam (Type u_5)) [] [] [Module R M] [Module S M₂] [FunLike F M M₂] extends , :

ContinuousSemilinearMapClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear maps M → M₂. See also ContinuousLinearMapClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Instances
@[reducible, inline]
abbrev ContinuousLinearMapClass (F : Type u_1) (R : outParam (Type u_2)) [] (M : outParam (Type u_3)) [] [] (M₂ : outParam (Type u_4)) [] [] [Module R M] [Module R M₂] [FunLike F M M₂] :

ContinuousLinearMapClass F R M M₂ asserts F is a type of bundled continuous R-linear maps M → M₂. This is an abbreviation for ContinuousSemilinearMapClass F (RingHom.id R) M M₂.

Equations
Instances For
structure ContinuousLinearEquiv {R : Type u_1} {S : Type u_2} [] [] (σ : R →+* S) {σ' : S →+* R} [] [] (M : Type u_3) [] [] (M₂ : Type u_4) [] [] [Module R M] [Module S M₂] extends :
Type (max u_3 u_4)

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

• toFun : MM₂
• map_add' : ∀ (x y : M), (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' : ∀ (m : R) (x : M), (↑self.toLinearEquiv).toFun (m x) = σ m (↑self.toLinearEquiv).toFun x
• invFun : M₂M
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• continuous_toFun : Continuous (↑self.toLinearEquiv).toFun

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

• continuous_invFun : Continuous self.invFun

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Instances For
theorem ContinuousLinearEquiv.continuous_toFun {R : Type u_1} {S : Type u_2} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_3} [] [] {M₂ : Type u_4} [] [] [Module R M] [Module S M₂] (self : M ≃SL[σ] M₂) :
Continuous (↑self.toLinearEquiv).toFun

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

theorem ContinuousLinearEquiv.continuous_invFun {R : Type u_1} {S : Type u_2} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_3} [] [] {M₂ : Type u_4} [] [] [Module R M] [Module S M₂] (self : M ≃SL[σ] M₂) :
Continuous self.invFun

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

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

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class ContinuousSemilinearEquivClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [] [] (σ : outParam (R →+* S)) {σ' : outParam (S →+* R)} [] [] (M : outParam (Type u_4)) [] [] (M₂ : outParam (Type u_5)) [] [] [Module R M] [Module S M₂] [EquivLike F M M₂] extends :

ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

• map_add : ∀ (f : F) (a b : M), f (a + b) = f a + f b
• map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r x) = σ r f x
• map_continuous : ∀ (f : F),

ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

• inv_continuous : ∀ (f : F),

ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Instances
theorem ContinuousSemilinearEquivClass.map_continuous {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [] [] {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [] [] {M : outParam (Type u_4)} [] [] {M₂ : outParam (Type u_5)} [] [] [Module R M] [Module S M₂] [EquivLike F M M₂] [self : ] (f : F) :

ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

theorem ContinuousSemilinearEquivClass.inv_continuous {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [] [] {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [] [] {M : outParam (Type u_4)} [] [] {M₂ : outParam (Type u_5)} [] [] [Module R M] [Module S M₂] [EquivLike F M M₂] [self : ] (f : F) :

ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

@[reducible, inline]
abbrev ContinuousLinearEquivClass (F : Type u_1) (R : outParam (Type u_2)) [] (M : outParam (Type u_3)) [] [] (M₂ : outParam (Type u_4)) [] [] [Module R M] [Module R M₂] [EquivLike F M M₂] :

ContinuousLinearEquivClass F σ M M₂ asserts F is a type of bundled continuous R-linear equivs M → M₂. This is an abbreviation for ContinuousSemilinearEquivClass F (RingHom.id R) M M₂.

Equations
Instances For
@[instance 100]
instance ContinuousSemilinearEquivClass.continuousSemilinearMapClass (F : Type u_1) {R : Type u_2} {S : Type u_3} [] [] (σ : R →+* S) {σ' : S →+* R} [] [] (M : Type u_4) [] [] (M₂ : Type u_5) [] [] [Module R M] [Module S M₂] [EquivLike F M M₂] [s : ] :
Equations
• =
@[simp]
theorem linearMapOfMemClosureRangeCoe_apply {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [] [T2Space M₂] [] [] [] [] [Module R M₁] [Module S M₂] [] [] {σ : R →+* S} (f : M₁M₂) (hf : f closure (Set.range DFunLike.coe)) :
= (↑).toFun
def linearMapOfMemClosureRangeCoe {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [] [T2Space M₂] [] [] [] [] [Module R M₁] [Module S M₂] [] [] {σ : R →+* S} (f : M₁M₂) (hf : f closure (Set.range DFunLike.coe)) :
M₁ →ₛₗ[σ] M₂

Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.

Equations
• = let __src := ; { toFun := (↑__src).toFun, map_add' := , map_smul' := }
Instances For
@[simp]
theorem linearMapOfTendsto_apply {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [] [T2Space M₂] [] [] [] [] [Module R M₁] [Module S M₂] [] [] {σ : R →+* S} {l : } (f : M₁M₂) (g : αM₁ →ₛₗ[σ] M₂) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :
(linearMapOfTendsto f g h) = f
def linearMapOfTendsto {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [] [T2Space M₂] [] [] [] [] [Module R M₁] [Module S M₂] [] [] {σ : R →+* S} {l : } (f : M₁M₂) (g : αM₁ →ₛₗ[σ] M₂) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :
M₁ →ₛₗ[σ] M₂

Construct a bundled linear map from a pointwise limit of linear maps

Equations
Instances For
theorem LinearMap.isClosed_range_coe (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [] [T2Space M₂] [] [] [] [] [Module R M₁] [Module S M₂] [] [] (σ : R →+* S) :
IsClosed (Set.range DFunLike.coe)

### Properties that hold for non-necessarily commutative semirings. #

instance ContinuousLinearMap.LinearMap.coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂)

Coerce continuous linear maps to linear maps.

Equations
• ContinuousLinearMap.LinearMap.coe = { coe := ContinuousLinearMap.toLinearMap }
theorem ContinuousLinearMap.coe_injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
Function.Injective ContinuousLinearMap.toLinearMap
instance ContinuousLinearMap.funLike {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
FunLike (M₁ →SL[σ₁₂] M₂) M₁ M₂
Equations
• ContinuousLinearMap.funLike = { coe := fun (f : M₁ →SL[σ₁₂] M₂) => f, coe_injective' := }
instance ContinuousLinearMap.continuousSemilinearMapClass {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂
Equations
• =
theorem ContinuousLinearMap.coe_mk {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : Continuous f.toFun) :
{ toLinearMap := f, cont := h } = f

Coerce continuous linear maps to functions.

@[simp]
theorem ContinuousLinearMap.coe_mk' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : Continuous f.toFun) :
{ toLinearMap := f, cont := h } = f
theorem ContinuousLinearMap.continuous {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
theorem ContinuousLinearMap.uniformContinuous {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {E₁ : Type u_9} {E₂ : Type u_10} [] [] [] [] [Module R₁ E₁] [Module R₂ E₂] [] [] (f : E₁ →SL[σ₁₂] E₂) :
@[simp]
theorem ContinuousLinearMap.coe_inj {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} :
f = g f = g
theorem ContinuousLinearMap.coeFn_injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
Function.Injective DFunLike.coe
def ContinuousLinearMap.Simps.apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :
M₁M₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
Instances For
def ContinuousLinearMap.Simps.coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :
M₁ →ₛₗ[σ₁₂] M₂

See Note [custom simps projection].

Equations
Instances For
theorem ContinuousLinearMap.ext_iff {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} :
f = g ∀ (x : M₁), f x = g x
theorem ContinuousLinearMap.ext {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} (h : ∀ (x : M₁), f x = g x) :
f = g
def ContinuousLinearMap.copy {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁M₂) (h : f' = f) :
M₁ →SL[σ₁₂] M₂

Copy of a ContinuousLinearMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = { toLinearMap := (↑f).copy f' h, cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.coe_copy {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁M₂) (h : f' = f) :
(f.copy f' h) = f'
theorem ContinuousLinearMap.copy_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁M₂) (h : f' = f) :
f.copy f' h = f
theorem ContinuousLinearMap.map_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
f 0 = 0
theorem ContinuousLinearMap.map_add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (x : M₁) (y : M₁) :
f (x + y) = f x + f y
theorem ContinuousLinearMap.map_smulₛₗ {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) :
f (c x) = σ₁₂ c f x
theorem ContinuousLinearMap.map_smul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) :
f (c x) = c f x
@[simp]
theorem ContinuousLinearMap.map_smul_of_tower {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {R : Type u_9} {S : Type u_10} [] [SMul R M₁] [Module S M₁] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁) :
f (c x) = c f x
@[deprecated map_sum]
theorem ContinuousLinearMap.map_sum {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {ι : Type u_9} (f : M₁ →SL[σ₁₂] M₂) (s : ) (g : ιM₁) :
f (∑ is, g i) = is, f (g i)
@[simp]
theorem ContinuousLinearMap.coe_coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
f = f
theorem ContinuousLinearMap.ext_ring_iff {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] {f : R₁ →L[R₁] M₁} {g : R₁ →L[R₁] M₁} :
f = g f 1 = g 1
theorem ContinuousLinearMap.ext_ring {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] {f : R₁ →L[R₁] M₁} {g : R₁ →L[R₁] M₁} (h : f 1 = g 1) :
f = g
theorem ContinuousLinearMap.eqOn_closure_span {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [T2Space M₂] {s : Set M₁} {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn (⇑f) (⇑g) s) :
Set.EqOn (⇑f) (⇑g) (closure (Submodule.span R₁ s))

If two continuous linear maps are equal on a set s, then they are equal on the closure of the Submodule.span of this set.

theorem ContinuousLinearMap.ext_on {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [T2Space M₂] {s : Set M₁} (hs : Dense (Submodule.span R₁ s)) {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn (⇑f) (⇑g) s) :
f = g

If the submodule generated by a set s is dense in the ambient module, then two continuous linear maps equal on s are equal.

theorem Submodule.topologicalClosure_map {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] [] [] [ContinuousSMul R₁ M₁] [] [ContinuousSMul R₂ M₂] [] (f : M₁ →SL[σ₁₂] M₂) (s : Submodule R₁ M₁) :
Submodule.map (↑f) s.topologicalClosure (Submodule.map (↑f) s).topologicalClosure

Under a continuous linear map, the image of the TopologicalClosure of a submodule is contained in the TopologicalClosure of its image.

theorem DenseRange.topologicalClosure_map_submodule {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] [] [] [ContinuousSMul R₁ M₁] [] [ContinuousSMul R₂ M₂] [] {f : M₁ →SL[σ₁₂] M₂} (hf' : ) {s : Submodule R₁ M₁} (hs : s.topologicalClosure = ) :
(Submodule.map (↑f) s).topologicalClosure =

Under a dense continuous linear map, a submodule whose TopologicalClosure is ⊤ is sent to another such submodule. That is, the image of a dense set under a map with dense range is dense.

instance ContinuousLinearMap.instSMul {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] :
SMul S₂ (M₁ →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.instSMul = { smul := fun (c : S₂) (f : M₁ →SL[σ₁₂] M₂) => { toLinearMap := c f, cont := } }
instance ContinuousLinearMap.mulAction {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] :
MulAction S₂ (M₁ →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.mulAction =
theorem ContinuousLinearMap.smul_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(c f) x = c f x
@[simp]
theorem ContinuousLinearMap.coe_smul {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
(c f) = c f
@[simp]
theorem ContinuousLinearMap.coe_smul' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
(c f) = c f
instance ContinuousLinearMap.isScalarTower {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [Monoid S₂] [Monoid T₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] [DistribMulAction T₂ M₂] [SMulCommClass R₂ T₂ M₂] [] [SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] :
IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂)
Equations
• =
instance ContinuousLinearMap.smulCommClass {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [Monoid S₂] [Monoid T₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [] [DistribMulAction T₂ M₂] [SMulCommClass R₂ T₂ M₂] [] [SMulCommClass S₂ T₂ M₂] :
SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂)
Equations
• =
instance ContinuousLinearMap.zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
Zero (M₁ →SL[σ₁₂] M₂)

The continuous map that is constantly zero.

Equations
• ContinuousLinearMap.zero = { zero := { toLinearMap := 0, cont := } }
instance ContinuousLinearMap.inhabited {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
Inhabited (M₁ →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.inhabited = { default := 0 }
@[simp]
theorem ContinuousLinearMap.default_def {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
default = 0
@[simp]
theorem ContinuousLinearMap.zero_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (x : M₁) :
0 x = 0
@[simp]
theorem ContinuousLinearMap.coe_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
0 = 0
theorem ContinuousLinearMap.coe_zero' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] :
0 = 0
instance ContinuousLinearMap.uniqueOfLeft {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] :
Unique (M₁ →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.uniqueOfLeft = .unique
instance ContinuousLinearMap.uniqueOfRight {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] :
Unique (M₁ →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.uniqueOfRight = .unique
theorem ContinuousLinearMap.exists_ne_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} (hf : f 0) :
∃ (x : M₁), f x 0
def ContinuousLinearMap.id (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [] [] [Module R₁ M₁] :
M₁ →L[R₁] M₁

the identity map as a continuous linear map.

Equations
• = { toLinearMap := LinearMap.id, cont := }
Instances For
instance ContinuousLinearMap.one {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] :
One (M₁ →L[R₁] M₁)
Equations
• ContinuousLinearMap.one = { one := }
theorem ContinuousLinearMap.one_def {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] :
1 =
theorem ContinuousLinearMap.id_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (x : M₁) :
(ContinuousLinearMap.id R₁ M₁) x = x
@[simp]
theorem ContinuousLinearMap.coe_id {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] :
(ContinuousLinearMap.id R₁ M₁) = LinearMap.id
@[simp]
theorem ContinuousLinearMap.coe_id' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] :
(ContinuousLinearMap.id R₁ M₁) = id
@[simp]
theorem ContinuousLinearMap.coe_eq_id {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] {f : M₁ →L[R₁] M₁} :
f = LinearMap.id f =
@[simp]
theorem ContinuousLinearMap.one_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (x : M₁) :
1 x = x
instance ContinuousLinearMap.instNontrivialId {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
Nontrivial (M₁ →L[R₁] M₁)
Equations
• =
instance ContinuousLinearMap.add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] :
Equations
• ContinuousLinearMap.add = { add := fun (f g : M₁ →SL[σ₁₂] M₂) => { toLinearMap := f + g, cont := } }
@[simp]
theorem ContinuousLinearMap.add_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] (f : M₁ →SL[σ₁₂] M₂) (g : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(f + g) x = f x + g x
@[simp]
theorem ContinuousLinearMap.coe_add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] (f : M₁ →SL[σ₁₂] M₂) (g : M₁ →SL[σ₁₂] M₂) :
(f + g) = f + g
theorem ContinuousLinearMap.coe_add' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] (f : M₁ →SL[σ₁₂] M₂) (g : M₁ →SL[σ₁₂] M₂) :
(f + g) = f + g
instance ContinuousLinearMap.addCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] :
Equations
@[simp]
theorem ContinuousLinearMap.coe_sum {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] {ι : Type u_9} (t : ) (f : ιM₁ →SL[σ₁₂] M₂) :
(∑ dt, f d) = dt, (f d)
@[simp]
theorem ContinuousLinearMap.coe_sum' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] {ι : Type u_9} (t : ) (f : ιM₁ →SL[σ₁₂] M₂) :
(∑ dt, f d) = dt, (f d)
theorem ContinuousLinearMap.sum_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] {ι : Type u_9} (t : ) (f : ιM₁ →SL[σ₁₂] M₂) (b : M₁) :
(∑ dt, f d) b = dt, (f d) b
def ContinuousLinearMap.comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
M₁ →SL[σ₁₃] M₃

Composition of bounded linear maps.

Equations
• g.comp f = { toLinearMap := (↑g).comp f, cont := }
Instances For

Composition of bounded linear maps.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousLinearMap.coe_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(h.comp f) = (↑h).comp f
@[simp]
theorem ContinuousLinearMap.coe_comp' {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(h.comp f) = h f
theorem ContinuousLinearMap.comp_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(g.comp f) x = g (f x)
@[simp]
theorem ContinuousLinearMap.comp_id {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
f.comp (ContinuousLinearMap.id R₁ M₁) = f
@[simp]
theorem ContinuousLinearMap.id_comp {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
(ContinuousLinearMap.id R₂ M₂).comp f = f
@[simp]
theorem ContinuousLinearMap.comp_zero {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) :
g.comp 0 = 0
@[simp]
theorem ContinuousLinearMap.zero_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem ContinuousLinearMap.comp_add {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] [] (g : M₂ →SL[σ₂₃] M₃) (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₁ →SL[σ₁₂] M₂) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
@[simp]
theorem ContinuousLinearMap.add_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] (g₁ : M₂ →SL[σ₂₃] M₃) (g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem ContinuousLinearMap.comp_assoc {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] {M₄ : Type u_8} [] [] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_9} [Semiring R₄] [Module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄) (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(h.comp g).comp f = h.comp (g.comp f)
instance ContinuousLinearMap.instMul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] :
Mul (M₁ →L[R₁] M₁)
Equations
• ContinuousLinearMap.instMul = { mul := ContinuousLinearMap.comp }
theorem ContinuousLinearMap.mul_def {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (g : M₁ →L[R₁] M₁) :
f * g = f.comp g
@[simp]
theorem ContinuousLinearMap.coe_mul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (g : M₁ →L[R₁] M₁) :
(f * g) = f g
theorem ContinuousLinearMap.mul_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (g : M₁ →L[R₁] M₁) (x : M₁) :
(f * g) x = f (g x)
instance ContinuousLinearMap.monoidWithZero {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] :
MonoidWithZero (M₁ →L[R₁] M₁)
Equations
• ContinuousLinearMap.monoidWithZero =
theorem ContinuousLinearMap.coe_pow {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (n : ) :
(f ^ n) = (⇑f)^[n]
instance ContinuousLinearMap.instNatCast {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
NatCast (M₁ →L[R₁] M₁)
Equations
• ContinuousLinearMap.instNatCast = { natCast := fun (n : ) => n 1 }
instance ContinuousLinearMap.semiring {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
Semiring (M₁ →L[R₁] M₁)
Equations
@[simp]
theorem ContinuousLinearMap.toLinearMapRingHom_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] (self : M₁ →L[R₁] M₁) :
ContinuousLinearMap.toLinearMapRingHom self = self
def ContinuousLinearMap.toLinearMapRingHom {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
(M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁

ContinuousLinearMap.toLinearMap as a RingHom.

Equations
• ContinuousLinearMap.toLinearMapRingHom = { toFun := ContinuousLinearMap.toLinearMap, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem ContinuousLinearMap.natCast_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] (n : ) (m : M₁) :
n m = n m
@[simp]
theorem ContinuousLinearMap.ofNat_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] (n : ) [n.AtLeastTwo] (m : M₁) :
(OfNat.ofNat n) m = m
instance ContinuousLinearMap.applyModule {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
Module (M₁ →L[R₁] M₁) M₁

The tautological action by M₁ →L[R₁] M₁ on M.

This generalizes Function.End.applyMulAction.

Equations
• ContinuousLinearMap.applyModule = Module.compHom M₁ ContinuousLinearMap.toLinearMapRingHom
@[simp]
theorem ContinuousLinearMap.smul_def {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] (f : M₁ →L[R₁] M₁) (a : M₁) :
f a = f a
instance ContinuousLinearMap.applyFaithfulSMul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
FaithfulSMul (M₁ →L[R₁] M₁) M₁

ContinuousLinearMap.applyModule is faithful.

Equations
• =
instance ContinuousLinearMap.applySMulCommClass {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
SMulCommClass R₁ (M₁ →L[R₁] M₁) M₁
Equations
• =
instance ContinuousLinearMap.applySMulCommClass' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁
Equations
• =
instance ContinuousLinearMap.continuousConstSMul_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] :
ContinuousConstSMul (M₁ →L[R₁] M₁) M₁
Equations
• =
def ContinuousLinearMap.prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :
M₁ →L[R₁] M₂ × M₃

The cartesian product of two bounded linear maps, as a bounded linear map.

Equations
• f₁.prod f₂ = { toLinearMap := (↑f₁).prod f₂, cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.coe_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :
(f₁.prod f₂) = (↑f₁).prod f₂
@[simp]
theorem ContinuousLinearMap.prod_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) (x : M₁) :
(f₁.prod f₂) x = (f₁ x, f₂ x)
def ContinuousLinearMap.inl (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [] [] (M₂ : Type u_6) [] [] [Module R₁ M₁] [Module R₁ M₂] :
M₁ →L[R₁] M₁ × M₂

The left injection into a product is a continuous linear map.

Equations
Instances For
def ContinuousLinearMap.inr (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [] [] (M₂ : Type u_6) [] [] [Module R₁ M₁] [Module R₁ M₂] :
M₂ →L[R₁] M₁ × M₂

The right injection into a product is a continuous linear map.

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.inl_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] (x : M₁) :
(ContinuousLinearMap.inl R₁ M₁ M₂) x = (x, 0)
@[simp]
theorem ContinuousLinearMap.inr_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] (x : M₂) :
(ContinuousLinearMap.inr R₁ M₁ M₂) x = (0, x)
@[simp]
theorem ContinuousLinearMap.coe_inl {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.inl R₁ M₁ M₂) = LinearMap.inl R₁ M₁ M₂
@[simp]
theorem ContinuousLinearMap.coe_inr {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.inr R₁ M₁ M₂) = LinearMap.inr R₁ M₁ M₂
theorem ContinuousLinearMap.isClosed_ker {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] {F : Type u_9} [T1Space M₂] [FunLike F M₁ M₂] [ContinuousSemilinearMapClass F σ₁₂ M₁ M₂] (f : F) :
theorem ContinuousLinearMap.isComplete_ker {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [] [] [Module R₂ M₂] {F : Type u_9} {M' : Type u_10} [] [] [] [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) :
instance ContinuousLinearMap.completeSpace_ker {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [] [] [Module R₂ M₂] {F : Type u_9} {M' : Type u_10} [] [] [] [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) :
Equations
• =
instance ContinuousLinearMap.completeSpace_eqLocus {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [] [] [Module R₂ M₂] {F : Type u_9} {M' : Type u_10} [] [] [] [Module R₁ M'] [T2Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) (g : F) :
Equations
• =
@[simp]
theorem ContinuousLinearMap.ker_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
LinearMap.ker (f.prod g) =
def ContinuousLinearMap.codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x p) :
M₁ →SL[σ₁₂] p

Restrict codomain of a continuous linear map.

Equations
Instances For
theorem ContinuousLinearMap.coe_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x p) :
(f.codRestrict p h) = LinearMap.codRestrict p (↑f) h
@[simp]
theorem ContinuousLinearMap.coe_codRestrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x p) (x : M₁) :
((f.codRestrict p h) x) = f x
@[simp]
theorem ContinuousLinearMap.ker_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x p) :
LinearMap.ker (f.codRestrict p h) =
@[reducible, inline]
abbrev ContinuousLinearMap.rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] (f : M₁ →SL[σ₁₂] M₂) :
M₁ →SL[σ₁₂]

Restrict the codomain of a continuous linear map f to f.range.

Equations
• f.rangeRestrict = f.codRestrict
Instances For
@[simp]
theorem ContinuousLinearMap.coe_rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₂ M₂] [] (f : M₁ →SL[σ₁₂] M₂) :
f.rangeRestrict = (↑f).rangeRestrict
def Submodule.subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (p : Submodule R₁ M₁) :
p →L[R₁] M₁

Submodule.subtype as a ContinuousLinearMap.

Equations
• p.subtypeL = { toLinearMap := p.subtype, cont := }
Instances For
@[simp]
theorem Submodule.coe_subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (p : Submodule R₁ M₁) :
p.subtypeL = p.subtype
@[simp]
theorem Submodule.coe_subtypeL' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (p : Submodule R₁ M₁) :
p.subtypeL = p.subtype
@[simp]
theorem Submodule.subtypeL_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (p : Submodule R₁ M₁) (x : p) :
p.subtypeL x = x
@[simp]
theorem Submodule.range_subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (p : Submodule R₁ M₁) :
LinearMap.range p.subtypeL = p
@[simp]
theorem Submodule.ker_subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] (p : Submodule R₁ M₁) :
LinearMap.ker p.subtypeL =
def ContinuousLinearMap.fst (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [] [] (M₂ : Type u_6) [] [] [Module R₁ M₁] [Module R₁ M₂] :
M₁ × M₂ →L[R₁] M₁

Prod.fst as a ContinuousLinearMap.

Equations
Instances For
def ContinuousLinearMap.snd (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [] [] (M₂ : Type u_6) [] [] [Module R₁ M₁] [Module R₁ M₂] :
M₁ × M₂ →L[R₁] M₂

Prod.snd as a ContinuousLinearMap.

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.coe_fst {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.fst R₁ M₁ M₂) = LinearMap.fst R₁ M₁ M₂
@[simp]
theorem ContinuousLinearMap.coe_fst' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.fst R₁ M₁ M₂) = Prod.fst
@[simp]
theorem ContinuousLinearMap.coe_snd {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.snd R₁ M₁ M₂) = LinearMap.snd R₁ M₁ M₂
@[simp]
theorem ContinuousLinearMap.coe_snd' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.snd R₁ M₁ M₂) = Prod.snd
@[simp]
theorem ContinuousLinearMap.fst_prod_snd {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] [Module R₁ M₁] [Module R₁ M₂] :
(ContinuousLinearMap.fst R₁ M₁ M₂).prod (ContinuousLinearMap.snd R₁ M₁ M₂) = ContinuousLinearMap.id R₁ (M₁ × M₂)
@[simp]
theorem ContinuousLinearMap.fst_comp_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
(ContinuousLinearMap.fst R₁ M₂ M₃).comp (f.prod g) = f
@[simp]
theorem ContinuousLinearMap.snd_comp_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
(ContinuousLinearMap.snd R₁ M₂ M₃).comp (f.prod g) = g
def ContinuousLinearMap.prodMap {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] {M₄ : Type u_8} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :
M₁ × M₃ →L[R₁] M₂ × M₄

Prod.map of two continuous linear maps.

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.coe_prodMap {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] {M₄ : Type u_8} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :
(f₁.prodMap f₂) = (↑f₁).prodMap f₂
@[simp]
theorem ContinuousLinearMap.coe_prodMap' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] {M₄ : Type u_8} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :
(f₁.prodMap f₂) = Prod.map f₁ f₂
def ContinuousLinearMap.coprod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :
M₁ × M₂ →L[R₁] M₃

The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.

Equations
• f₁.coprod f₂ = { toLinearMap := (↑f₁).coprod f₂, cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.coe_coprod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :
(f₁.coprod f₂) = (↑f₁).coprod f₂
@[simp]
theorem ContinuousLinearMap.coprod_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) (x : M₁ × M₂) :
(f₁.coprod f₂) x = f₁ x.1 + f₂ x.2
theorem ContinuousLinearMap.range_coprod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :
LinearMap.range (f₁.coprod f₂) =
theorem ContinuousLinearMap.comp_fst_add_comp_snd {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {M₃ : Type u_7} [] [] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [] (f : M₁ →L[R₁] M₃) (g : M₂ →L[R₁] M₃) :
f.comp (ContinuousLinearMap.fst R₁ M₁ M₂) + g.comp (ContinuousLinearMap.snd R₁ M₁ M₂) = f.coprod g
theorem ContinuousLinearMap.coprod_inl_inr {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] {M'₁ : Type u_5} [] [] [Module R₁ M₁] [Module R₁ M'₁] [] [] :
(ContinuousLinearMap.inl R₁ M₁ M'₁).coprod (ContinuousLinearMap.inr R₁ M₁ M'₁) = ContinuousLinearMap.id R₁ (M₁ × M'₁)
def ContinuousLinearMap.smulRight {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {R : Type u_10} {S : Type u_11} [] [] [Module R M₁] [Module R M₂] [Module R S] [Module S M₂] [IsScalarTower R S M₂] [] [] (c : M₁ →L[R] S) (f : M₂) :
M₁ →L[R] M₂

The linear map fun x => c x • f. Associates to a scalar-valued linear map and an element of M₂ the M₂-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂). See also ContinuousLinearMap.smulRightₗ and ContinuousLinearMap.smulRightL.

Equations
• c.smulRight f = let __src := (↑c).smulRight f; { toLinearMap := __src, cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.smulRight_apply {M₁ : Type u_4} [] [] {M₂ : Type u_6} [] [] {R : Type u_10} {S : Type u_11} [] [] [Module R M₁] [Module R M₂] [Module R S] [Module S M₂] [IsScalarTower R S M₂] [] [] {c : M₁ →L[R] S} {f : M₂} {x : M₁} :
(c.smulRight f) x = c x f
@[simp]
theorem ContinuousLinearMap.smulRight_one_one {R₁ : Type u_1} [Semiring R₁] {M₂ : Type u_6} [] [] [Module R₁ M₂] [] [ContinuousSMul R₁ M₂] (c : R₁ →L[R₁] M₂) :
= c
@[simp]
theorem ContinuousLinearMap.smulRight_one_eq_iff {R₁ : Type u_1} [Semiring R₁] {M₂ : Type u_6} [] [] [Module R₁ M₂] [] [ContinuousSMul R₁ M₂] {f : M₂} {f' : M₂} :
f = f'
theorem ContinuousLinearMap.smulRight_comp {R₁ : Type u_1} [Semiring R₁] {M₂ : Type u_6} [] [] [Module R₁ M₂] [] [ContinuousSMul R₁ M₂] [] {x : M₂} {c : R₁} :
.comp =
def ContinuousLinearMap.toSpanSingleton (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] [ContinuousSMul R₁ M₁] (x : M₁) :
R₁ →L[R₁] M₁

Given an element x of a topological space M over a semiring R, the natural continuous linear map from R to M by taking multiples of x.

Equations
• = { toLinearMap := , cont := }
Instances For
theorem ContinuousLinearMap.toSpanSingleton_apply (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] [ContinuousSMul R₁ M₁] (x : M₁) (r : R₁) :
= r x
theorem ContinuousLinearMap.toSpanSingleton_add (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] [ContinuousSMul R₁ M₁] [] (x : M₁) (y : M₁) :
theorem ContinuousLinearMap.toSpanSingleton_smul' (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] [] [ContinuousSMul R₁ M₁] {α : Type u_10} [] [] [] [SMulCommClass R₁ α M₁] (c : α) (x : M₁) :
theorem ContinuousLinearMap.toSpanSingleton_smul (R : Type u_10) {M₁ : Type u_11} [] [] [Module R M₁] [] [] [] (c : R) (x : M₁) :

A special case of to_span_singleton_smul' for when R is commutative.

def ContinuousLinearMap.pi {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :
M →L[R] (i : ι) → φ i

pi construction for continuous linear functions. From a family of continuous linear functions it produces a continuous linear function into a family of topological modules.

Equations
• = { toLinearMap := LinearMap.pi fun (i : ι) => (f i), cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.coe_pi' {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :
= fun (c : M) (i : ι) => (f i) c
@[simp]
theorem ContinuousLinearMap.coe_pi {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :
= LinearMap.pi fun (i : ι) => (f i)
theorem ContinuousLinearMap.pi_apply {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) (c : M) (i : ι) :
c i = (f i) c
theorem ContinuousLinearMap.pi_eq_zero {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :
∀ (i : ι), f i = 0
theorem ContinuousLinearMap.pi_zero {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
(ContinuousLinearMap.pi fun (x : ι) => 0) = 0
theorem ContinuousLinearMap.pi_comp {R : Type u_1} [] {M : Type u_2} [] [] [Module R M] {M₂ : Type u_3} [] [] [Module R M₂] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) (g : M₂ →L[R] M) :
.comp g = ContinuousLinearMap.pi fun (i : ι) => (f i).comp g
def ContinuousLinearMap.proj {R : Type u_1} [] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) :
((i : ι) → φ i) →L[R] φ i

The projections from a family of topological modules are continuous linear maps.

Equations
• = { toLinearMap := , cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.proj_apply {R : Type u_1} [] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) :
= b i
theorem ContinuousLinearMap.proj_pi {R : Type u_1} [] {M₂ : Type u_3} [] [] [Module R M₂] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →L[R] φ i) (i : ι) :
.comp = f i
theorem ContinuousLinearMap.iInf_ker_proj {R : Type u_1} [] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
⨅ (i : ι), =
def Pi.compRightL (R : Type u_1) [] {ι : Type u_4} (φ : ιType u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {α : Type u_6} (f : αι) :
((i : ι) → φ i) →L[R] (i : α) → φ (f i)

Given a function f : α → ι, it induces a continuous linear function by right composition on product types. For f = Subtype.val, this corresponds to forgetting some set of variables.

Equations
• = { toFun := fun (v : (i : ι) → φ i) (i : α) => v (f i), map_add' := , map_smul' := , cont := }
Instances For
@[simp]
theorem Pi.compRightL_apply (R : Type u_1) [] {ι : Type u_4} (φ : ιType u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {α : Type u_6} (f : αι) (v : (i : ι) → φ i) (i : α) :
(Pi.compRightL R φ f) v i = v (f i)
def ContinuousLinearMap.iInfKerProjEquiv (R : Type u_1) [] {ι : Type u_4} (φ : ιType u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {J : Set ι} [DecidablePred fun (i : ι) => i I] (hd : Disjoint I J) (hu : Set.univ I J) :
(⨅ iJ, ) ≃L[R] (i : I) → φ i

If I and J are complementary index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.

Equations
• = { toLinearEquiv := , continuous_toFun := , continuous_invFun := }
Instances For
theorem ContinuousLinearMap.map_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M) :
f (-x) = -f x
theorem ContinuousLinearMap.map_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M) (y : M) :
f (x - y) = f x - f y
@[simp]
theorem ContinuousLinearMap.sub_apply' {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) (x : M) :
(f - g) x = f x - g x
theorem ContinuousLinearMap.range_prod_eq {R : Type u_1} [Ring R] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R M₂] [Module R M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} (h : ) :
LinearMap.range (f.prod g) = .prod
theorem ContinuousLinearMap.ker_prod_ker_le_ker_coprod {R : Type u_1} [Ring R] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R M₂] [Module R M₃] [] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
.prod LinearMap.ker (f.coprod g)
theorem ContinuousLinearMap.ker_coprod_of_disjoint_range {R : Type u_1} [Ring R] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R M₂] [Module R M₃] [] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) (hd : ) :
LinearMap.ker (f.coprod g) = .prod
instance ContinuousLinearMap.neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Neg (M →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.neg = { neg := fun (f : M →SL[σ₁₂] M₂) => { toLinearMap := -f, cont := } }
@[simp]
theorem ContinuousLinearMap.neg_apply {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →SL[σ₁₂] M₂) (x : M) :
(-f) x = -f x
@[simp]
theorem ContinuousLinearMap.coe_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →SL[σ₁₂] M₂) :
(-f) = -f
theorem ContinuousLinearMap.coe_neg' {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →SL[σ₁₂] M₂) :
(-f) = -f
instance ContinuousLinearMap.sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Sub (M →SL[σ₁₂] M₂)
Equations
• ContinuousLinearMap.sub = { sub := fun (f g : M →SL[σ₁₂] M₂) => { toLinearMap := f - g, cont := } }
instance ContinuousLinearMap.addCommGroup {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Equations
theorem ContinuousLinearMap.sub_apply {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) (x : M) :
(f - g) x = f x - g x
@[simp]
theorem ContinuousLinearMap.coe_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) :
(f - g) = f - g
@[simp]
theorem ContinuousLinearMap.coe_sub' {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) :
(f - g) = f - g
@[simp]
theorem ContinuousLinearMap.comp_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] [] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
g.comp (-f) = -g.comp f
@[simp]
theorem ContinuousLinearMap.neg_comp {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
(-g).comp f = -g.comp f
@[simp]
theorem ContinuousLinearMap.comp_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] [] (g : M₂ →SL[σ₂₃] M₃) (f₁ : M →SL[σ₁₂] M₂) (f₂ : M →SL[σ₁₂] M₂) :
g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂
@[simp]
theorem ContinuousLinearMap.sub_comp {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [] [] {M₂ : Type u_5} [] [] {M₃ : Type u_6} [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] (g₁ : M₂ →SL[σ₂₃] M₃) (g₂ : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
(g₁ - g₂).comp f = g₁.comp f - g₂.comp f
instance ContinuousLinearMap.ring {R : Type u_1} [Ring R] {M :