div

Mathlib.Algebra.Order.Nonneg.Field

URI: https://scilib.ai/kg/mathlib#Nonneg.div

English

Division is defined pointwise on the nonnegative subtype: (x,hx) / (y,hy) = (x/y, div_nonneg hx hy).

Русский

Деление определено поэлементно на подтипе неотрицательных: (x,hx) / (y,hy) = (x/y, div_nonneg hx hy).

LaTeX

$$$\\frac{(x, hx)}{(y, hy)} = (\\tfrac{x}{y}, \\mathrm{div\\_nonneg}\\; hx\, hy)$$$

Lean4

instance div : Div { x : α // 0 ≤ x } :=
  ⟨fun x y => ⟨x / y, div_nonneg x.2 y.2⟩⟩

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

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

Разделы

Аффилиация

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