one_add_kstar_mul_self_eq_kstar

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.one_add_kstar_mul_self_eq_kstar

English

One plus the product of l^* and l equals l^*: 1 + l^* · l = l^*.

Русский

Ещё на единицу больше произведения л^* и л равно л^*: 1 + l^* · l = l^*.

LaTeX

$$1 + l^{\\ast} \\cdot l = l^{\\ast}$$

Lean4

@[simp]
theorem one_add_kstar_mul_self_eq_kstar (l : Language α) : 1 + l∗ * l = l∗ := by
  rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]

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

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

Разделы

Аффилиация

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