sum_ne_zero_of_injOn_supDegree — Mathlib

English

If s ≠ ∅, each f_i ≠ 0, and the map s → supDegree D ∘ f is injOn, then the sum ∑_{i∈s} f_i ≠ 0.

Русский

Если s не пусто, все f_i не равны нулю и отображение injOn для supDegree, то сумма не равна нулю.

LaTeX

$$s \neq \emptyset \to (∀ i ∈ s, f_i \neq 0) \to ( (s : Finset).InjOn (supDegree D \circ f) ) → ∑_{i∈s} f_i \neq 0$$

Lean4

theorem sum_ne_zero_of_injOn_supDegree (hs : s ≠ ∅) (hf : ∀ i ∈ s, f i ≠ 0) (hd : (s : Set ι).InjOn (supDegree D ∘ f)) :
    ∑ i ∈ s, f i ≠ 0 :=
  let ⟨i, hi⟩ := Finset.nonempty_iff_ne_empty.2 hs
  sum_ne_zero_of_injOn_supDegree' ⟨i, hi, hf i hi⟩ hd

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