co_support_zero — Mathlib

English

For every g, the set of indices a with the coefficient of g in (0)^a is nonzero is contained in {0}; i.e., only possibly the a=0 term can contribute nonzero to the zero series.

Русский

Для каждого g множество индексов a с ненулевым коэффициентом при g в (0)^a содержится в {0}; то есть только возможно член a=0 может дать ненулевой вклад в нулевую серию.

LaTeX

$$$\{a \mid ((0 : HahnSeries Γ R)^a).coeff(g) \neq 0\} \subseteq \{0\}$$$

Lean4

theorem co_support_zero [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (g : Γ) :
    {a | ¬((0 : HahnSeries Γ R) ^ a).coeff g = 0} ⊆ {0} :=
  by
  simp only [Set.subset_singleton_iff, Set.mem_setOf_eq]
  intro n hn
  by_contra h'
  simp_all only [ne_eq, not_false_eq_true, zero_pow, coeff_zero, not_true_eq_false]

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