ι_mem_evenOdd_one — Mathlib

English

Let Q be a quadratic form on a module M over a commutative ring R. In the Clifford algebra graded by parity into even and odd parts, the image of any vector m ∈ M under the Clifford map ι_Q lies in the degree-1 (odd) component: ι_Q(m) ∈ evenOdd(Q,1).

Русский

Пусть Q — квадратичная форма на модуле M над коммутативным кольцом R. В клиффордовой алгебре, градуированной по чётности на чётную и нечётную части, образ вектора m ∈ M под отображением ι_Q принадлежит компоненте степени 1: ι_Q(m) ∈ evenOdd(Q,1).

LaTeX

$$$\\iota_Q(m) \\in \\mathrm{evenOdd}(Q,1)$$$

Lean4

theorem ι_mem_evenOdd_one (m : M) : ι Q m ∈ evenOdd Q 1 :=
  range_ι_le_evenOdd_one Q <| LinearMap.mem_range_self _ m

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