comp_toLinearMap — Mathlib

English

The linear map underlying the composition of two AlgHoms equals the composition of their underlying linear maps: (g ∘ f).toLinearMap = g.toLinearMap ∘ f.toLinearMap.

Русский

Линейное отображение, связанное с заменой g и f, удовлетворяет: (g ∘ f).toLinearMap = g.toLinearMap ∘ f.toLinearMap.

LaTeX

$$$$(g\cdot f)^{\mathrm{toLinearMap}} = g^{\mathrm{toLinearMap}} \circ f^{\mathrm{toLinearMap}},$$$$

Lean4

@[simp]
theorem comp_toLinearMap (f : A →ₐ[R] B) (g : B →ₐ[R] C) : (g.comp f).toLinearMap = g.toLinearMap.comp f.toLinearMap :=
  rfl

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