even — Mathlib

English

The even submodule of a Clifford algebra is itself a subalgebra.

Русский

Чётная подмодуля клиффордовой алгебры сам по себе образует подалгебру.

LaTeX

$$def even : Subalgebra R (CliffordAlgebra Q)$$

Lean4

/-- The even submodule `CliffordAlgebra.evenOdd Q 0` is also a subalgebra. -/
def even : Subalgebra R (CliffordAlgebra Q) :=
  (evenOdd Q 0).toSubalgebra (SetLike.one_mem_graded _) fun _x _y hx hy =>
    add_zero (0 : ZMod 2) ▸ SetLike.mul_mem_graded hx hy

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