even_toSubmodule — Mathlib

English

The even subalgebra as a subalgebra coincides with the underlying even submodule image; i.e., even Q is the same as evenOdd Q 0 when viewed as subalgebras/submodules.

Русский

Чётвая подалгебра совпадает с соответствующей подмодулевой частью: even Q эквивалентно evenOdd Q 0 при рассмотрении как подалгебры/подмодуля.

LaTeX

$$$\text{even Q} \; = \; (\text{evenOdd } Q\; 0)\,\text{ as subalgebras and submodules}$$$

Lean4

@[simp]
theorem even_toSubmodule : Subalgebra.toSubmodule (even Q) = evenOdd Q 0 :=
  rfl

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