kstar_mul_kstar

Mathlib.Algebra.Order.Kleene

URI: https://scilib.ai/kg/mathlib#kstar_mul_kstar

← MathLib Explorer

English

(a^*)^* = a^*.

Русский

(a^*)^* = a^*.

LaTeX

$$$(a^*)^* = a^*$$$

Lean4

@[simp]
theorem kstar_mul_kstar (a : α) : a∗ * a∗ = a∗ :=
  (mul_kstar_le le_rfl <| kstar_mul_le_kstar).antisymm <| le_mul_of_one_le_left' one_le_kstar

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

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

Разделы

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

Аффилиация

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