pow_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- An element `a` is right-regular if and only if a positive power of `a` is right-regular. -/
@[to_additive]
theorem pow_iff (n0 : 0 < n) : IsRightRegular (a ^ n) ↔ IsRightRegular a
    where
  mp := by rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']; exact .of_mul
  mpr := .pow n

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