comp_assoc — Mathlib

English

The composition of three semilinear maps is associative: (h ∘ g) ∘ f = h ∘ (g ∘ f).

Русский

Объединение трёх полилинейных отображений ассоциативно: (h ∘ g) ∘ f = h ∘ (g ∘ f).

LaTeX

$$$((h \circ g) \circ f) = (h \circ (g \circ f)).$$$

Lean4

theorem comp_assoc {R₄ M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄}
    {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
    (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
    ((h.comp g : M₂ →ₛₗ[σ₂₄] M₄).comp f : M₁ →ₛₗ[σ₁₄] M₄) = h.comp (g.comp f : M₁ →ₛₗ[σ₁₃] M₃) :=
  rfl

Похожие утверждения