ι_mul_ι_comm — Mathlib

English

The commutator of ι_Q a and ι_Q b is governed by the polar form and the algebra map: ι_Q a ι_Q b = polar(Q)(a,b) − ι_Q b ι_Q a.

Русский

Коммутатор элементов ι_Q a и ι_Q b определяется через полярную форму и отображение: ι_Q a ι_Q b = polar(Q)(a,b) − ι_Q b ι_Q a.

LaTeX

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

Lean4

theorem ι_mul_ι_comm (a b : M) : ι Q a * ι Q b = algebraMap R _ (QuadraticMap.polar Q a b) - ι Q b * ι Q a :=
  eq_sub_of_add_eq (ι_mul_ι_add_swap a b)

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