compl₂_apply — Mathlib

English

A specialized variant of the identity composition for bilinear maps in the same framework.

Русский

Специализированный вариант композиции с идентичностью для билинейных отображений.

LaTeX

$$$$ h.compl₂ LinearMap.id = h $$$$

Lean4

@[simp]
theorem compl₂_apply (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) : h.compl₂ g m q = h m (g q) :=
  rfl

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