toUnits_injective

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

URI: https://scilib.ai/kg/mathlib#pinGroup.toUnits_injective

English

The map toUnits is injective.

Русский

Отображение toUnits инъективно.

LaTeX

$$toUnits is injective$$

Lean4

theorem toUnits_injective : Function.Injective (toUnits : pinGroup Q → (CliffordAlgebra Q)ˣ) := fun _x _y h =>
  Subtype.ext <| Units.ext_iff.mp h

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

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

Разделы

Аффилиация

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