pow — Mathlib

English

For any n > 0, a^n is M-regular if and only if a is M-regular.

Русский

При любом n > 0, a^n является M-регулярным тогда и только тогда, когда a является M-регулярным.

LaTeX

$$$0 < n \Rightarrow IsSMulRegular M (a^n) \iff IsSMulRegular M a$$$

Lean4

/-- Any power of an `M`-regular element is `M`-regular. -/
theorem pow (n : ℕ) (ra : IsSMulRegular M a) : IsSMulRegular M (a ^ n) := by
  induction n with
  | zero => rw [pow_zero]; simp only [one]
  | succ n hn =>
    rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn

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