pow — Mathlib

English

If a is idempotent in a monoid, then a^n is idempotent for every n ∈ ℕ.

Русский

Если a идемпотентен в мономе, то a^n идемпотентно для каждого n ∈ ℕ.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\; \\text{IsIdempotentElem}(a^n).$$$

Lean4

theorem pow (n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n) :=
  Nat.recOn n ((pow_zero a).symm ▸ one) fun n _ =>
    show a ^ n.succ * a ^ n.succ = a ^ n.succ by
      conv_rhs => rw [← h.eq]
      rw [← sq, ← sq, ← pow_mul, ← pow_mul']

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