instDivSubtypeMemAddSubgroup — Mathlib

English

The self-adjoint elements are closed under division: if x,y are self-adjoint and y ≠ 0, then x/y is self-adjoint.

Русский

Самосопряжённые элементы замкнуты относительно деления: если x,y самосопряжённы и y ≠ 0, то x/y самосопряжён.

LaTeX

$$$IsSelfAdjoint(x) \land IsSelfAdjoint(y) \to IsSelfAdjoint\left(\dfrac{x}{y}\right)$$$

Lean4

instance : Div (selfAdjoint R) where div x y := ⟨x / y, x.prop.div y.prop⟩

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