star_eq_inv'

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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

English

The same statement as star equals inverse, but stated with the Inv.inv form.

Русский

То же утверждение в форме Inv.inv.

LaTeX

$$star x = x^{-1}$$

Lean4

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

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

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

Разделы

Аффилиация

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