units_involute_act_eq_conjAct — Mathlib

English

For a unit x ∈ spinGroup Q and any y in M, involute x acts by conjAct on ι Q y equal to standard action.

Русский

Для единицы x ∈ spinGroup Q и любого y ∈ M действие involute x через conjAct на ι Q y совпадает со стандартным действием.

LaTeX

$$involute (Q := Q) ↑x * ι Q y * ↑x⁻¹ = ConjAct.toConjAct x • (ι Q y)$$

Lean4

theorem units_involute_act_eq_conjAct {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ spinGroup Q) (y : M) :
    involute (Q := Q) ↑x * ι Q y * ↑x⁻¹ = ConjAct.toConjAct x • (ι Q y) := by
  rw [involute_eq hx, @ConjAct.units_smul_def, @ConjAct.ofConjAct_toConjAct]

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