pow — Mathlib

English

Any power a^n of a right-regular element a is right-regular.

Русский

Любая степень a^n правой регулярности a также является правой регулярностью.

LaTeX

$$$ IsRightRegular a \rightarrow IsRightRegular (a^n) $$$

Lean4

/-- Any power of a right-regular element is right-regular. -/
@[to_additive]
theorem pow (n : ℕ) (rra : IsRightRegular a) : IsRightRegular (a ^ n) :=
  by
  rw [IsRightRegular, ← mul_right_iterate]
  exact rra.iterate n

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