mem_iff

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

URI: https://scilib.ai/kg/mathlib#spinGroup.mem_iff

← MathLib Explorer

English

If x is in spinGroup, then x also lies in CliffordAlgebra.even Q.

Русский

Если x ∈ spinGroup, то x ∈ CliffordAlgebra.even Q.

LaTeX

$$x ∈ even Q$$

Lean4

/-- An element is in `spinGroup Q` if and only if it is in `pinGroup Q` and `even Q`. -/
theorem mem_iff {x : CliffordAlgebra Q} : x ∈ spinGroup Q ↔ x ∈ pinGroup Q ∧ x ∈ even Q :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru