oneFunc

Mathlib.ModelTheory.Algebra.Ring.Basic

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

← MathLib Explorer

English

The constant one operation in the ring is denoted by oneFunc, i.e., oneFunc() = 1.

Русский

Константа единицы в кольце обозначается oneFunc и равна единице.

LaTeX

$$$$ \text{oneFunc} = 1. $$$$

Lean4

/-- `RingFunc.one`, but with the defeq type `Language.ring.Functions 0` instead
of `RingFunc 0` -/
abbrev oneFunc : Language.ring.Functions 0 :=
  one

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

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

Разделы

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

Аффилиация

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