natDegree_multiset_prod_X_sub_C_eq_card

English

For a multiset s ⊆ R, natDegree of ∏_{x∈s} (X − C x) equals card(s).

Русский

Для мультимножества s ⊆ R natDegree(∏_{x∈s} (X − C x)) равно.card(s).

LaTeX

$$$$\operatorname{natDegree}\left(\prod_{x\in s} (X - C x)\right) = |s|.$$$$

Lean4

@[simp]
theorem natDegree_multiset_prod_X_sub_C_eq_card (s : Multiset R) : (s.map (X - C ·)).prod.natDegree = Multiset.card s :=
  by
  rw [natDegree_multiset_prod_of_monic, Multiset.map_map]
  · simp only [(· ∘ ·), natDegree_X_sub_C, Multiset.map_const', Multiset.sum_replicate, smul_eq_mul, mul_one]
  · exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a

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