coeff_ne_zero_of_le — Mathlib

English

If coeff R p m f ≠ 0 and m ≤ n, then coeff R p n f ≠ 0.

Русский

Если coeff R p m f ≠ 0 и m ≤ n, то coeff R p n f ≠ 0.

LaTeX

$$$\\text{coeff } R p m f \\neq 0 \\land (m \\le n) \\implies \\text{coeff } R p n f \\neq 0$$$

Lean4

theorem coeff_ne_zero_of_le {f : Ring.Perfection R p} {m n : ℕ} (hfm : coeff R p m f ≠ 0) (hmn : m ≤ n) :
    coeff R p n f ≠ 0 :=
  let ⟨k, hk⟩ := Nat.exists_eq_add_of_le hmn
  hk.symm ▸ coeff_add_ne_zero hfm k

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