English
Under mild assumptions, the self-adjoint elements form a field with the same algebraic operations as the ambient ring.
Русский
При разумных предпосылках самосопряжённые элементы образуют поле с теми же операциями, что и в окружающем кольце.
LaTeX
$$$ \\{ x \\in R \\mid x^{*} = x \\} \\text{ образуют подполе } R. $$$
Lean4
instance instField : Field (selfAdjoint R) :=
Subtype.coe_injective.field _ (selfAdjoint R).coe_zero val_one (selfAdjoint R).coe_add val_mul (selfAdjoint R).coe_neg
(selfAdjoint R).coe_sub val_inv val_div (swap (selfAdjoint R).coe_nsmul) (by intros; rfl) val_nnqsmul val_qsmul
val_pow val_zpow (fun _ => rfl) (fun _ => rfl) val_nnratCast val_ratCast
