spanCoeffs_ne_top — Mathlib

English

The span of all coefficients of subProdXSubC f across all monics is a proper ideal; i.e., spanCoeffs(k) ≠ ⊤.

Русский

Порождение всех коэффициентов subProdXSubC(f) по всем моникам образует правильный идеал; spanCoeffs(k) ≠ ⊤.

LaTeX

$$spanCoeffs(k) ≠ ⊤$$

Lean4

theorem spanCoeffs_ne_top : spanCoeffs k ≠ ⊤ :=
  by
  rw [Ideal.ne_top_iff_one, spanCoeffs, Ideal.span, ← Set.image_univ, Finsupp.mem_span_image_iff_linearCombination]
  rintro ⟨v, _, hv⟩
  classical
  replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv
  rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv
  · exact zero_ne_one hv
  intro j hj
  rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]

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