pow_eq

Mathlib.Algebra.Star.StarProjection

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

English

If p is a star projection and n ≠ 0, then p^n = p.

Русский

Если p — звездная проекция и n ≠ 0, то p^n = p.

LaTeX

$$$ p^n = p \quad\text{for all } n \in \mathbb{N},\ n \neq 0. $$$

Lean4

theorem pow_eq [Monoid R] [Star R] (hp : IsStarProjection p) {n : ℕ} (hn : n ≠ 0) : p ^ n = p :=
  hp.isIdempotentElem.pow_eq hn

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

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

Разделы

Аффилиация

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