symmCompOfNondegenerate_left_apply

English

For a nondegenerate B, the construction leftAdjointOfNondegenerate b φ gives a left adjoint of φ with respect to B, i.e., IsAdjointPair B B (leftAdjointOfNondegenerate b φ) φ.

Русский

Для невырожденной B построение leftAdjointOfNondegenerate b φ дает левый сопряженный пары к φ по отношению к B.

LaTeX

$$IsAdjointPair(B,B, B.leftAdjointOfNondegenerate b φ, φ)$$

Lean4

@[simp]
theorem symmCompOfNondegenerate_left_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V} (b₂ : B₂.Nondegenerate) (v w : V) :
    B₂ (symmCompOfNondegenerate B₁ B₂ b₂ w) v = B₁ w v := by conv_lhs => rw [comp_symmCompOfNondegenerate_apply]

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