pow_succ_eq

Mathlib.Algebra.Star.StarProjection

URI: https://scilib.ai/kg/mathlib#IsStarProjection.pow_succ_eq

English

For a star projection p, p^{n+1} = p for all n.

Русский

Для звездной проекции p выполняется p^{n+1} = p для всех n.

LaTeX

$$$ p^{n+1} = p $$$

Lean4

theorem pow_succ_eq [Monoid R] [Star R] (hp : IsStarProjection p) (n : ℕ) : p ^ (n + 1) = p :=
  hp.isIdempotentElem.pow_succ_eq n

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

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

Разделы

Аффилиация

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