ne_zero_iff_exists_coeff_ne_zero_and_weight

English

A mv-power-series f is nonzero if and only if there exist indices n ∈ ℕ and d ∈ σ →₀ ℕ such that coeff d f ≠ 0 and weight w d = n.

Русский

mv-ряд не нулевой тогда и только тогда, когда существуют индексы n и d такие, что коэффициент d f ≠ 0 и вес d равен n.

LaTeX

$$$f \neq 0 \iff (\exists n:\mathbb{N}, \exists d:\, \sigma \to\_0\mathbb{N},\; \mathrm{coeff}(d,f) \neq 0 \land \mathrm{weight}(w,d)=n).$$$

Lean4

theorem ne_zero_iff_exists_coeff_ne_zero_and_weight : f ≠ 0 ↔ (∃ n : ℕ, ∃ d : σ →₀ ℕ, coeff d f ≠ 0 ∧ weight w d = n) :=
  by
  refine not_iff_not.mp ?_
  simp only [ne_eq, not_not, not_exists, not_and, forall_apply_eq_imp_iff₂, imp_false]
  exact MvPowerSeries.ext_iff

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