lcomp_apply — Mathlib

English

Let f: M → M′ and g: M′ → N be linear maps over a common ring. Then the composition in the bilinear construction equals ordinary composition, i.e. for every x in M, (lcomp S N f g)(x) = g(f(x]).

Русский

Пусть f: M → M′ и g: M′ → N — линейные отображения над общей кольцевой структурой. Тогда композиция в билинейном конструировании равна обычной композиции: для каждого x ∈ M выполняется (lcomp S N f g)(x) = g(f(x)).

LaTeX

$$$ \\forall x\\in M,\\ (lcomp S N f g)(x) = g\\big(f(x)\\big). $$$

Lean4

@[simp]
theorem lcomp_apply (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] N) (x : M) : lcomp S N f g x = g (f x) :=
  rfl

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