instAdd

Mathlib.Algebra.Order.Ring.Archimedean

URI: https://scilib.ai/kg/mathlib#ArchimedeanClass.instAdd

← MathLib Explorer

English

mk(xy) equals mk x plus mk y.

Русский

mk(xy) равно mk x плюс mk y.

LaTeX

$$$$ \operatorname{mk}(xy) = \operatorname{mk}(x) + \operatorname{mk}(y). $$$$

Lean4

/-- Multipilication in `R` transfers to Addition in `ArchimedeanClass R`. -/
instance : Add (ArchimedeanClass R) where
  add :=
    lift₂ (fun x y ↦ .mk <| x * y) fun _ _ _ _ hx hy ↦
      (mk_mul_le_of_le hx.le hy.le).antisymm (mk_mul_le_of_le hx.ge hy.ge)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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