instInvSubtypeMemAddSubgroup

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#selfAdjoint.instInvSubtypeMemAddSubgroup

English

In a field, the inverse of a self-adjoint element is self-adjoint.

Русский

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

LaTeX

$$$IsSelfAdjoint(x) \Rightarrow IsSelfAdjoint(x^{-1})$$$

Lean4

instance : Inv (selfAdjoint R) where inv x := ⟨x.val⁻¹, x.prop.inv₀⟩

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

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

Разделы

Аффилиация

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