Theorems · Theorem · field theory
AlgebraicClosure.Monics.splits_finsetProd
∀ {k : Type u} [inst : Field k] {s : Finset (AlgebraicClosure.Monics k)} {f : AlgebraicClosure.Monics k},
f ∈ s → (Polynomial.map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).Splits- Cited by
- 1 results in Mathlib
- Foundations
- Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement · cited by 5,681
- Algebra.algebraMapstatement and proof · cited by 4,706
- Finset.prodstatement and proof · cited by 2,356
- Polynomial.mapstatement · cited by 806
- Polynomial.Monicstatement · cited by 461
- Polynomial.Splitsstatement and proof · cited by 290
- Polynomial.Monic.ne_zeroproof · cited by 63
- Polynomial.SplittingFieldstatement and proof · cited by 42
- Polynomial.map_ne_zeroproof · cited by 22
- Polynomial.SplittingField.splitsproof · cited by 21
Cited by1
Results whose statement or proof uses this declaration.
- AlgebraicClosure.toSplittingField_coeffproof · cited by 1