kstar_eq_self

Mathlib.Algebra.Order.Kleene

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

← MathLib Explorer

English

a^* = a iff a · a = a and 1 ≤ a.

Русский

a^* = a тогда и только если a · a = a и 1 ≤ a.

LaTeX

$$$a^* = a \iff a \cdot a = a \land 1 \le a$$$

Lean4

@[simp]
theorem kstar_eq_self : a∗ = a ↔ a * a = a ∧ 1 ≤ a :=
  ⟨fun h ↦ ⟨by rw [← h, kstar_mul_kstar], one_le_kstar.trans_eq h⟩, fun h ↦
    (kstar_le_of_mul_le_left h.2 h.1.le).antisymm le_kstar⟩

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

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

Разделы

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

Аффилиация

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