addFunc

Mathlib.ModelTheory.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#FirstOrder.Ring.addFunc

← MathLib Explorer

English

The binary operation of addition on a ring is denoted by addFunc, i.e., addFunc(x,y) = x + y.

Русский

Двоичное сложение в кольце задаётся операцией, обозначаемой addFunc: addFunc(x,y) = x + y.

LaTeX

$$$$ \text{addFunc}(x,y) = x + y. $$$$

Lean4

/-- `RingFunc.add`, but with the defeq type `Language.ring.Functions 2` instead
of `RingFunc 2` -/
abbrev addFunc : Language.ring.Functions 2 :=
  add

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

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

Разделы

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

Аффилиация

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