hasZero

Mathlib.Algebra.FreeAlgebra

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

English

An upper bound by the max of R, X and aleph0 holds in general.

Русский

Общее верхнее ограничение через максимум R, X и aleph0.

LaTeX

$$ #(FreeAlgebra R X) ≤ #R ⊔ #X ⊔ ℵ₀$$

Lean4

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

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

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

Разделы

Аффилиация

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