comp_symmCompOfNondegenerate_apply

English

With B1, B2 as above, B2 (symmCompOfNondegenerate B1 B2 b2 w) applied to v equals B1 w v.

Русский

С учетом B1, B2, B2 (symmCompOfNondegenerate B1 B2 b2 w) применяется к v, тогда B1 w v = B2(...).

LaTeX

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

Lean4

theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V} (b₂ : B₂.Nondegenerate) (v : V) :
    B₂ (B₁.symmCompOfNondegenerate B₂ b₂ v) = B₁ v :=
  by
  rw [symmCompOfNondegenerate]
  simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
  erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)]

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