cardinalMk_eq_one

Mathlib.Algebra.FreeAlgebra.Cardinality

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.cardinalMk_eq_one

← MathLib Explorer

English

If R is a subsingleton then all FreeAlgebra constructions have cardinality 1.

Русский

Если R является подсупермным, то кардинал FreeAlgebra равно 1.

LaTeX

$$$[Subsingleton R] \\Rightarrow \\#(FreeAlgebra R X) = 1$$$

Lean4

@[nontriviality]
theorem cardinalMk_eq_one [Subsingleton R] : #(FreeAlgebra R X) = 1 := by
  rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_eq_one]

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

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

Разделы

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

Аффилиация

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