inv₀

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.inv₀

English

In a group with zero, the inverse of a self-adjoint element is self-adjoint.

Русский

В группе с нулём обратный самосопряжённого элемента самосопряжён.

LaTeX

$$$\text{IsSelfAdjoint}(x) \rightarrow \text{IsSelfAdjoint}(x^{-1})$$$

Lean4

@[aesop safe apply]
theorem inv₀ {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint x⁻¹ := by
  simp only [isSelfAdjoint_iff, star_inv₀, hx.star_eq]

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

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

Разделы

Аффилиация

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