symmCompOfNondegenerate — Mathlib

English

For bilinear forms B1,B2 with B2 nondegenerate, the composition B2.symmCompOfNondegenerate B1 b2 applied to v yields a linear functional equal to B1 applied to v, i.e., B2((B1.symmCompOfNondegenerate B2 b2) v) = B1 v.

Русский

Для билинейных форм B1,B2 с B2 невырожденной композиция B2.symmCompOfNondegenerate B1 b2 примененная к v дает линейную функциональную форму, равную B1 v: B2((B1.symmCompOfNondegenerate B2 b2) v) = B1 v.

LaTeX

$$$B_2\\big(B_1^{\\mathrm{symmCompOfNondegenerate}}(B_2,b_2)\\, v\\big) = B_1 v$$$

Lean4

/-- Given bilinear forms `B₁, B₂` where `B₂` is nondegenerate, `symmCompOfNondegenerate`
is the linear map `B₂ ∘ B₁`. -/
noncomputable def symmCompOfNondegenerate (B₁ B₂ : BilinForm K V) (b₂ : B₂.Nondegenerate) : V →ₗ[K] V :=
  (B₂.toDual b₂).symm.toLinearMap.comp B₁

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