neg_e0_mul_v — Mathlib

English

The new-dimension unit vector e0 anticommutes with the original embedding v: −(e0 · v(m)) = v(m) · e0 for all m ∈ M.

Русский

Единичный вектор новой размерности e0 антикоммутирует с встройкой исходного пространства: −(e0 · v(m)) = v(m) · e0 для всех m ∈ M.

LaTeX

$$$-(e_0(Q) \\cdot v_Q(m)) = v_Q(m) \\cdot e_0(Q)$$$

Lean4

theorem neg_e0_mul_v (m : M) : -(e0 Q * v Q m) = v Q m * e0 Q :=
  by
  refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_)
  dsimp [QuadraticMap.polar]
  simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero, add_sub_cancel_right, sub_self, map_zero]

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