instAddCommMagma

Mathlib.Algebra.Order.Ring.Archimedean

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

← MathLib Explorer

English

Addition in ArchimedeanClass R is commutative: x + y = y + x.

Русский

Сложение в ArchimedeanClass R коммутативно: x + y = y + x.

LaTeX

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

Lean4

instance : AddCommMagma (ArchimedeanClass R) where
  add_comm x
    y :=
    by
    induction x with
    | mk x
    induction y with
    | mk y
    rw [← mk_mul, mul_comm, mk_mul]

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

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

Разделы

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

Аффилиация

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