English
Let M be a monoid and k a natural number with 1 < k. Suppose P : M → Prop satisfies: (i) for all x,y ∈ M, P x implies P (x · y) or P (y · x); (ii) for all x ∈ M, P (x^k) implies P x. Then for every n ∈ ℕ and x ∈ M, P (x^n) implies P x.
Русский
Пусть M — моноид, k ∈ ℕ и 1 < k. Пусть P : M → Prop удовлетворяет условиям: (i) для любых x,y ∈ M, P x ⇒ P (x · y) или P (y · x); (ii) для всех x ∈ M, P (x^k) ⇒ P x. Тогда для любых n ∈ ℕ и x ∈ M верно P (x^n) ⇒ P x.
LaTeX
$$$\\forall M [Monoid M] \, (k : \mathbb{N}) \, (hk : 1 < k) \, (P : M \to \mathrm{Prop}) \, (hmul : ∀ x y, P x \to (P (x \cdot y) \\lor P (y \cdot x))) \, (hpow : ∀ x, P (x^k) \to P x), \\forall n x, P (x^n) \to P x.$$$
Lean4
theorem pow_imp_self_of_one_lt {M} [Monoid M] (k : ℕ) (hk : 1 < k) (P : M → Prop)
(hmul : ∀ x y, P x → P (x * y) ∨ P (y * x)) (hpow : ∀ x, P (x ^ k) → P x) : ∀ n x, P (x ^ n) → P x :=
k.cauchy_induction_mul
(fun n ih x hx ↦ ih x <| (hmul _ x hx).elim (fun h ↦ by rwa [_root_.pow_succ]) fun h ↦ by rwa [_root_.pow_succ']) 0
hk (fun x hx ↦ pow_one x ▸ hx) fun n _ hn x hx ↦ hpow x <| hn _ <| (pow_mul x k n).subst hx
