comp_assoc — Mathlib

English

The composition of A →ₐ[R] B with C →ₐ[R] D is associative: for φ3: A →ₐ[R] B, φ2: B →ₐ[R] C, φ1: C →ₐ[R] D, we have (φ1 ∘ φ2) ∘ φ3 = φ1 ∘ (φ2 ∘ φ3).

Русский

Ассоциативность композиции алгебраических гомоморфизмов: для φ3: A →ₐ[R] B, φ2: B →ₐ[R] C, φ1: C →ₐ[R] D верно (φ1 ∘ φ2) ∘ φ3 = φ1 ∘ (φ2 ∘ φ3).

LaTeX

$$$$(\phi_1 \circ \phi_2) \circ \phi_3 = \phi_1 \circ (\phi_2 \circ \phi_3).$$$$

Lean4

theorem comp_assoc (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) : (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃) :=
  rfl

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