Theorems · Theorem · field theory
AlgebraicClosure.toSplittingField_coeff
∀ {k : Type u} [inst : Field k] {s : Finset (AlgebraicClosure.Monics k)} {f : AlgebraicClosure.Monics k},
f ∈ s → ∀ (n : ℕ), (AlgebraicClosure.toSplittingField s) ((AlgebraicClosure.subProdXSubC f).coeff n) = 0- Cited by
- 1 results in Mathlib
- Foundations
- Depth 157 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.
Cites57
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- RingHomproof · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Finsuppstatement · cited by 5,255
- Algebra.algebraMapproof · cited by 4,706
- Equiv.symmproof · cited by 3,681
- Finset.univproof · cited by 3,473
- AlgHomstatement · cited by 3,236
- one_mulproof · cited by 2,841
- Multisetproof · cited by 2,627
Cited by1
Results whose statement or proof uses this declaration.
- AlgebraicClosure.spanCoeffs_ne_topproof · cited by 1