Theorems · Theorem · functional analysis

LinearIsometry.comp_assoc

∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {R₄ : Type u_4} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7}
  {E₄ : Type u_8} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₄]
  {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_4 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_5 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
  [inst_6 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_7 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [inst_8 : SeminormedAddCommGroup E]
  [inst_9 : SeminormedAddCommGroup E₂] [inst_10 : SeminormedAddCommGroup E₃] [inst_11 : SeminormedAddCommGroup E₄]
  [inst_12 : Module R E] [inst_13 : Module R₂ E₂] [inst_14 : Module R₃ E₃] [inst_15 : Module R₄ E₄]
  (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂), (f.comp g).comp h = f.comp (g.comp h)

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

0 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringSemiringSemiringSemiringRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupSeminormedAddCommGroupModuleModuleModuleModule