mul_ι_mul_ι_of_isOrtho — Mathlib

English

For any x in a Clifford algebra element and any Q-orthogonal a,b, x ι_Q a ι_Q b = − (ι_Q b ι_Q a) x.

Русский

Для любого элемента x в клиффордовой алгебре и ортогональной пары a,b: x ι_Q a ι_Q b = − (ι_Q b ι_Q a) x.

LaTeX

$$$x \\cdot ι_Q a \\cdot ι_Q b = - (ι_Q b \\cdot ι_Q a) \\cdot x$ if $Q.IsOrtho(a,b)$.$$

Lean4

theorem mul_ι_mul_ι_of_isOrtho (x : CliffordAlgebra Q) {a b : M} (h : Q.IsOrtho a b) :
    x * ι Q a * ι Q b = -(x * ι Q b * ι Q a) := by rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]

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