Theorems · Theorem · field theory
Polynomial.monic_multiset_prod_of_monic
∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R),
(∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic- Defined in
- Mathlib.Algebra.Polynomial.Monic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement and proof · cited by 5,681
- Multisetstatement and proof · cited by 2,627
- Multiset.mapstatement and proof · cited by 876
- Multiset.prodstatement and proof · cited by 528
- Polynomial.Monicstatement and proof · cited by 461
- Multiset.consproof · cited by 313
- Multiset.induction_onproof · cited by 109
- Multiset.map_consproof · cited by 93
- Multiset.prod_consproof · cited by 68
- Multiset.mem_cons_selfproof · cited by 44
- Multiset.mem_cons_of_memproof · cited by 35
Cited by6
Results whose statement or proof uses this declaration.
- Polynomial.monic_prod_of_monicproof · cited by 12
- Polynomial.splits_iff_exists_multiset'proof · cited by 4
- Polynomial.monic_multisetProd_X_sub_Cproof · cited by 4
- Polynomial.Monic.nextCoeff_multiset_prodproof · cited by 3
- Polynomial.Splits.scaleRootsproof · cited by 1
- Polynomial.degree_multiset_prod_of_monicproof · cited by 1