compl₂ — Mathlib

English

Composing with identity returns the original bilinear map.

Русский

Композиция с тождественным отображением возвращает исходную билинейную форму.

LaTeX

$$$$ h.compl₂ \mathrm{Id} = h $$$$

Lean4

/-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
form a bilinear map `M → Q → P`. -/
def compl₂ (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P
    where
  toFun a := (lcompₛₗ R₅ P σ₂₃ g) (h a)
  map_add' _ _ := by simp [map_add]
  map_smul' _ _ := by simp [LinearMap.map_smulₛₗ, lcompₛₗ]

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