lcomp_apply' — Mathlib

English

As objects, the bilinear composition operator lcomp yields the same result as the ordinary composition of linear maps, i.e. lcomp S N f g equals g ∘ f as linear maps.

Русский

Как объекты, билинейное вложение lcomp равно обычной композиции линейных отображений: lcomp S N f g = g ∘ f.

LaTeX

$$$ lcomp S N f g = g \\circ f $$$

Lean4

theorem lcomp_apply' (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] N) : lcomp S N f g = g ∘ₗ f :=
  rfl

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