comp_toAlgHom — Mathlib

English

The algebra part of the composition equals the composition of the algebra parts.

Русский

Алгебраическая часть композиции равна композиции алгебраических частей.

LaTeX

$$$\\phi_1.comp \\phi_2 = (\\phi_1 : B \\to_{R}^{\\!a} C).comp (\\phi_2 : A \\to_{R}^{\\!a} B)$$$

Lean4

@[simp]
theorem comp_toAlgHom (φ₁ : B →ₐc[R] C) (φ₂ : A →ₐc[R] B) : φ₁.comp φ₂ = (φ₁ : B →ₐ[R] C).comp (φ₂ : A →ₐ[R] B) :=
  rfl

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