isUnit_ι_iff

Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.isUnit_ι_iff

English

Simplicity result: the unit-ness of ι_Q(m) is equivalent to the unit-ness of Q(m).

Русский

Упрощённый результат: обратимость ι_Q(m) эквивалентна обратимости Q(m).

LaTeX

$$isUnit_ι_iff(Q,m)$$

Lean4

@[simp]
theorem isUnit_ι_iff {m : M} : IsUnit (ι Q m) ↔ IsUnit (Q m) :=
  ⟨isUnit_of_isUnit_ι Q, isUnit_ι_of_isUnit Q⟩

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

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

Разделы

Аффилиация

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