coeff_nat_find_add_ne_zero — Mathlib

English

If there exists h with coeff nonzero, then coeff at find h + something is nonzero.

Русский

Если существует h с ненулевым коэффициентом, значит коэффициент на find h + сумма тоже ненулевой.

LaTeX

$$coeff(Perfection.coeff(...)(Nat.find h + k)) ≠ 0$$

Lean4

theorem coeff_nat_find_add_ne_zero {f : PreTilt O p} {h : ∃ n, coeff _ _ n f ≠ 0} (k : ℕ) :
    coeff _ _ (Nat.find h + k) f ≠ 0 :=
  coeff_add_ne_zero (Nat.find_spec h) k

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