pow_iff — Mathlib

English

IsRegular(a^n) iff IsRegular a for n > 0.

Русский

IsRegular(a^n) эквивалентно IsRegular a при n > 0.

LaTeX

$$$ IsRegular (a^n) \leftrightarrow IsRegular a \quad (0 < n) $$$

Lean4

/-- An element `a` is regular if and only if a positive power of `a` is regular. -/
@[to_additive]
theorem pow_iff {n : ℕ} (n0 : 0 < n) : IsRegular (a ^ n) ↔ IsRegular a
    where
  mp h := ⟨(IsLeftRegular.pow_iff n0).mp h.left, (IsRightRegular.pow_iff n0).mp h.right⟩
  mpr h := ⟨.pow n h.left, .pow n h.right⟩

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