pow_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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