star_iff — Mathlib

English

Star operation preserves idempotence: star(a) is idempotent iff a is idempotent.

Русский

Операция звезды сохраняет идемпотентность: star(a) идемпотентна тогда и только тогда, когда a идемпотентно.

LaTeX

$$IsIdempotentElem (star a) ⇔ IsIdempotentElem a$$

Lean4

theorem star_iff {R : Type*} [Mul R] [StarMul R] {a : R} : IsIdempotentElem (star a) ↔ IsIdempotentElem a := by
  simp [IsIdempotentElem, ← star_mul]

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