coeff_add_ne_zero — Mathlib

English

If coeff R p n f ≠ 0 for some f ∈ Ring.Perfection R p, then coeff R p (n+k) f ≠ 0 for all k ∈ ℕ.

Русский

Если коэффициент coeff R p n f ≠ 0 для некоторого f, то coeff R p (n+k) f ≠ 0 для всех k ∈ ℕ.

LaTeX

$$$\\text{coeff } R p n f \\neq 0 \\implies \\forall k,\\; \\text{coeff } R p (n+k) f \\neq 0$$$

Lean4

theorem coeff_add_ne_zero {f : Ring.Perfection R p} {n : ℕ} (hfn : coeff R p n f ≠ 0) (k : ℕ) :
    coeff R p (n + k) f ≠ 0 :=
  Nat.recOn k hfn fun k ih h =>
    ih <| by
      rw [Nat.add_succ] at h
      rw [← coeff_pow_p, RingHom.map_pow, h, zero_pow hp.1.ne_zero]

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