English
The function mapping m to weightedHomogeneousComponent w m φ has finite support; equivalently, the set of m with nonzero components is finite.
Русский
Функция m ↦ weightedHomogeneousComponent w m φ имеет конечную поддержку; то есть множество m с ненулевыми компонентами конечно.
LaTeX
$$(weightedHomogeneousComponent w · · φ).Finite$$
Lean4
/-- If `M` is a canonically `OrderedAddCommMonoid`, then the `weightedHomogeneousComponent`
of weighted degree `0` of a polynomial is its constant coefficient. -/
@[simp]
theorem weightedHomogeneousComponent_zero [CanonicallyOrderedAdd M] [NoZeroSMulDivisors ℕ M] (hw : ∀ i : σ, w i ≠ 0) :
weightedHomogeneousComponent w 0 φ = C (coeff 0 φ) := by
classical
ext1 d
rcases Classical.em (d = 0) with (rfl | hd)
· simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
· rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum, sum_eq_zero_iff,
Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or, and_self_left, exists_prop]
simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
obtain ⟨i, hi⟩ := hd
exact ⟨i, hi, hw i⟩
