monic_multiset_prod_of_monic — Mathlib

English

If p is monic, q ≠ 0 and natDegree q < natDegree p, then p does not divide q.

Русский

Если p моноическое, q ≠ 0 и natDegree q < natDegree p, то p не делится на q.

LaTeX

$$$Monic(p) \land q \neq 0 \land \operatorname{natDegree}(q) < \operatorname{natDegree}(p) \Rightarrow p \nmid q$$$

Lean4

theorem monic_multiset_prod_of_monic (t : Multiset ι) (f : ι → R[X]) (ht : ∀ i ∈ t, Monic (f i)) :
    Monic (t.map f).prod := by
  revert ht
  refine t.induction_on ?_ ?_; · simp
  intro a t ih ht
  rw [Multiset.map_cons, Multiset.prod_cons]
  exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))

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