ι_mul_ι_add_swap — Mathlib

English

The symmetric product of two images ι_Q a and ι_Q b equals a scalar given by the polar form; i.e., ι_Q a ι_Q b + ι_Q b ι_Q a = algebraMap_R (Clifford(Q))(polar(Q)(a,b)).

Русский

Симметрическая сумма произведений ι_Q a и ι_Q b равна скаляру, задаваемому полярной формой квадратичной формы.

LaTeX

$$$ι_Q a · ι_Q b + ι_Q b · ι_Q a = algebraMap_R (Clifford(Q)) (polar(Q)(a,b))$$$

Lean4

/-- The symmetric product of vectors is a scalar -/
theorem ι_mul_ι_add_swap (a b : M) : ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticMap.polar Q a b) :=
  mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _

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