exists_pow_smul_eq — Mathlib

English

From stability, there exists n0 with F.N(n0+k) = I^k · F.N(n0).

Русский

Из устойчивости следует существование n0 с F.N(n0+k) = I^k · F.N(n0).

LaTeX

$$∃ n₀, ∀ k, F.N(n₀+k) = I^k · F.N(n₀)$$

Lean4

theorem exists_pow_smul_eq (h : F.Stable) : ∃ n₀, ∀ k, F.N (n₀ + k) = I ^ k • F.N n₀ :=
  by
  obtain ⟨n₀, hn⟩ := h
  use n₀
  intro k
  induction k with
  | zero => simp
  | succ _ ih => rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]; cutsat

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