kstar_idem

Mathlib.Algebra.Order.Kleene

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

English

a** = a*.

Русский

a^{**} = a^*.

LaTeX

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

Lean4

@[simp]
theorem kstar_idem (a : α) : a∗∗ = a∗ :=
  kstar_eq_self.2 ⟨kstar_mul_kstar _, one_le_kstar⟩

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

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

Разделы

Аффилиация

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