star_eq_inv'

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

URI: https://scilib.ai/kg/mathlib#spinGroup.star_eq_inv'

English

The embedding toUnits is injective; distinct spinGroup elements map to distinct units in CliffordAlgebra.

Русский

Встраивание toUnits инъективно: разные элементы spinGroup отображаются в разные единицы CliffordAlgebra.

LaTeX

$$toUnits is injective: ∀ x ≠ y, toUnits(x) ≠ toUnits(y).$$

Lean4

theorem star_eq_inv' : (star : spinGroup Q → spinGroup Q) = Inv.inv :=
  rfl

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

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

Разделы

Аффилиация

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