inner_rightAngleRotationAux₁_left

English

For all vectors x and y in the real inner product space E, the inner product of the auxiliary right-angle rotation applied to x with y equals the area form evaluated at x and y: ⟨o.rightAngleRotationAux₁ x, y⟩ = ω(x, y).

Русский

Для всех векторов x, y в вещественном укрупненном(inner product space) E имеет место: ⟨o.rightAngleRotationAux₁ x, y⟩ = ω(x, y).

LaTeX

$$$\\\\langle o.rightAngleRotationAux₁ x, y\\\\rangle = \\omega(x, y)$$$

Lean4

@[simp]
theorem inner_rightAngleRotationAux₁_left (x y : E) : ⟪o.rightAngleRotationAux₁ x, y⟫ = ω x y :=
  by
  simp only [rightAngleRotationAux₁, LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearMap.coe_comp,
    LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply, LinearIsometryEquiv.coe_symm_toLinearEquiv]
  rw [InnerProductSpace.toDual_symm_apply]
  norm_cast

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