ne_zero_iff_exists_coeff_ne_zero_and_degree

English

f ≠ 0 iff there exists n and d with coeff d f ≠ 0 and degree d = n.

Русский

f ≠ 0 тогда существует n и d такие, что coeff d f ≠ 0 и degree d = n.

LaTeX

$$f ≠ 0 ↔ ∃ n, ∃ d, coeff d f ≠ 0 ∧ degree d = n$$

Lean4

theorem ne_zero_iff_exists_coeff_ne_zero_and_degree : f ≠ 0 ↔ (∃ n : ℕ, ∃ d : σ →₀ ℕ, coeff d f ≠ 0 ∧ degree d = n) :=
  by
  simp_rw [degree_eq_weight_one]
  exact ne_zero_iff_exists_coeff_ne_zero_and_weight (fun _ => 1)

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