hasMul

Mathlib.Algebra.FreeAlgebra

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

English

If X is empty, then the cardinality reduces to lift(#R).

Русский

Если X пусто, то мощность равна lift(#R).

LaTeX

$$$[IsEmpty X] \\Rightarrow \\#(FreeAlgebra R X) = \\operatorname{lift}(\\#R)$$$

Lean4

/-- Multiplication in `Pre R X` defined as `Pre.mul`. Note: Used for notation only. -/
def hasMul : Mul (Pre R X) :=
  ⟨mul⟩

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

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

Разделы

Аффилиация

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