pow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Any power of a left-regular element is left-regular. -/
@[to_additive]
theorem pow (n : ℕ) (rla : IsLeftRegular a) : IsLeftRegular (a ^ n) := by
  simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]

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