hasOne

Mathlib.Algebra.FreeAlgebra

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.Pre.hasOne

English

Under standard assumptions, the cardinality equals the maximum of #R, #X, and ℵ0.

Русский

При стандартных условиях мощность равна максимуму #R, #X и ℵ0.

LaTeX

$$$(Nonempty X) (Nontrivial R) ⇒ #(FreeAlgebra R X) = #R ⊔ #X ⊔ ℵ_0$$

Lean4

/-- One in `Pre R X` defined as the image of `1` from `R`. Note: Used for notation only. -/
def hasOne : One (Pre R X) :=
  ⟨ofScalar 1⟩

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

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

Разделы

Аффилиация

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