mulFunc

Mathlib.ModelTheory.Algebra.Ring.Basic

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

← MathLib Explorer

English

The binary operation of multiplication on a ring is denoted by mulFunc, i.e., mulFunc(x,y) = x · y.

Русский

Двоичное умножение в кольце обозначается mulFunc: mulFunc(x,y) = x·y.

LaTeX

$$$$ \text{mulFunc}(x,y) = x \cdot y. $$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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