Documentation

Mathlib.Topology.Algebra.Module.LinearMapPiProd

Continuous linear maps on products and Pi types #

Properties that hold for non-necessarily commutative semirings. #

def ContinuousLinearMap.prod {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid 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_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid 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_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] :
        (ContinuousLinearMap.inr R M₁ M₂) = LinearMap.inr R M₁ M₂
        @[simp]
        theorem ContinuousLinearMap.ker_prod {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) :
        def ContinuousLinearMap.fst (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid 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_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd M₃] (f₁ : M₁ →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
                LinearMap.range (f₁.coprod f₂) = LinearMap.range f₁ LinearMap.range f₂
                theorem ContinuousLinearMap.comp_fst_add_comp_snd {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd 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_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [ContinuousAdd M₁] [ContinuousAdd M₂] :
                (ContinuousLinearMap.inl R M₁ M₂).coprod (ContinuousLinearMap.inr R M₁ M₂) = ContinuousLinearMap.id R (M₁ × M₂)
                def ContinuousLinearMap.pi {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [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
                Instances For
                  @[simp]
                  theorem ContinuousLinearMap.coe_pi' {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [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) :
                  (ContinuousLinearMap.pi f) = fun (c : M) (i : ι) => (f i) c
                  @[simp]
                  theorem ContinuousLinearMap.coe_pi {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [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) :
                  (ContinuousLinearMap.pi f) = LinearMap.pi fun (i : ι) => (f i)
                  theorem ContinuousLinearMap.pi_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [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 : ι) :
                  (ContinuousLinearMap.pi f) c i = (f i) c
                  theorem ContinuousLinearMap.pi_eq_zero {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [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) :
                  ContinuousLinearMap.pi f = 0 ∀ (i : ι), f i = 0
                  theorem ContinuousLinearMap.pi_zero {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [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} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [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) :
                  (ContinuousLinearMap.pi f).comp g = ContinuousLinearMap.pi fun (i : ι) => (f i).comp g
                  def ContinuousLinearMap.proj {R : Type u_1} [Semiring R] {ι : 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
                  Instances For
                    @[simp]
                    theorem ContinuousLinearMap.proj_apply {R : Type u_1} [Semiring R] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) :
                    theorem ContinuousLinearMap.proj_pi {R : Type u_1} [Semiring R] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [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 : ι) :
                    theorem ContinuousLinearMap.iInf_ker_proj {R : Type u_1} [Semiring R] {ι : Type u_4} {φ : ιType u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :
                    def Pi.compRightL (R : Type u_1) [Semiring R] {ι : 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
                    • Pi.compRightL R φ f = { 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) [Semiring R] {ι : 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)
                      theorem ContinuousLinearMap.range_prod_eq {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} (h : LinearMap.ker f LinearMap.ker g = ) :
                      theorem ContinuousLinearMap.ker_prod_ker_le_ker_coprod {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃] [ContinuousAdd M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
                      (LinearMap.ker f).prod (LinearMap.ker g) LinearMap.ker (f.coprod g)
                      theorem ContinuousLinearMap.ker_coprod_of_disjoint_range {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃] [ContinuousAdd M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) (hd : Disjoint (LinearMap.range f) (LinearMap.range g)) :
                      LinearMap.ker (f.coprod g) = (LinearMap.ker f).prod (LinearMap.ker g)
                      def ContinuousLinearMap.prodEquiv {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] :
                      (M →L[R] M₂) × (M →L[R] M₃) (M →L[R] M₂ × M₃)

                      ContinuousLinearMap.prod as an Equiv.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem ContinuousLinearMap.prodEquiv_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (f : (M →L[R] M₂) × (M →L[R] M₃)) :
                        ContinuousLinearMap.prodEquiv f = f.1.prod f.2
                        theorem ContinuousLinearMap.prod_ext_iff {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {f g : M × M₂ →L[R] M₃} :
                        f = g f.comp (ContinuousLinearMap.inl R M M₂) = g.comp (ContinuousLinearMap.inl R M M₂) f.comp (ContinuousLinearMap.inr R M M₂) = g.comp (ContinuousLinearMap.inr R M M₂)
                        theorem ContinuousLinearMap.prod_ext {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {f g : M × M₂ →L[R] M₃} (hl : f.comp (ContinuousLinearMap.inl R M M₂) = g.comp (ContinuousLinearMap.inl R M M₂)) (hr : f.comp (ContinuousLinearMap.inr R M M₂) = g.comp (ContinuousLinearMap.inr R M M₂)) :
                        f = g
                        def ContinuousLinearMap.prodₗ {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (S : Type u_5) [Semiring S] [Module S M₂] [ContinuousAdd M₂] [SMulCommClass R S M₂] [ContinuousConstSMul S M₂] [Module S M₃] [ContinuousAdd M₃] [SMulCommClass R S M₃] [ContinuousConstSMul S M₃] :
                        ((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] M →L[R] M₂ × M₃

                        ContinuousLinearMap.prod as a LinearEquiv.

                        Equations
                        • ContinuousLinearMap.prodₗ S = { toFun := ContinuousLinearMap.prodEquiv.toFun, map_add' := , map_smul' := , invFun := ContinuousLinearMap.prodEquiv.invFun, left_inv := , right_inv := }
                        Instances For
                          @[simp]
                          theorem ContinuousLinearMap.prodₗ_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (S : Type u_5) [Semiring S] [Module S M₂] [ContinuousAdd M₂] [SMulCommClass R S M₂] [ContinuousConstSMul S M₂] [Module S M₃] [ContinuousAdd M₃] [SMulCommClass R S M₃] [ContinuousConstSMul S M₃] (a✝ : (M →L[R] M₂) × (M →L[R] M₃)) :
                          (ContinuousLinearMap.prodₗ S) a✝ = ContinuousLinearMap.prodEquiv.toFun a✝