val_div

Mathlib.Algebra.Star.SelfAdjoint

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

English

In the self-adjoint subtype, the value of x/y equals the division of their values.

Русский

В подмножестве самосопряжённых элементов значение x/y равно делению значений x и y.

LaTeX

$$$\forall x,y \in \mathrm{selfAdjoint}(R),\uparrow\left(\dfrac{x}{y}\right) = \dfrac{\uparrow x}{\uparrow y}$$$

Lean4

@[simp, norm_cast]
theorem val_div (x y : selfAdjoint R) : ↑(x / y) = (x / y : R) :=
  rfl

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

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

Разделы

Аффилиация

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