Mathlib Map

Theorems · Theorem · field theory

Polynomial.X_sub_C_mul_removeFactor

∀ {K : Type v} [inst : Field K] (f : Polynomial K),
  f.natDegree ≠ 0 →
    (Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor)) * f.removeFactor =
      Polynomial.map (AdjoinRoot.of f.factor) f
Defined in
Mathlib.FieldTheory.SplittingField.Construction
Cited by
2 results in Mathlib
Foundations
Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Field
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Polynomial.SplittingFieldAux.adjoin_rootSet · cited by 0SplittingFieldAux.adjoin_…Polynomial.SplittingFieldAux.splits · cited by 0SplittingFieldAux.splitsDFunLike.coe · cited by 62936DFunLike.coeRingHom · cited by 10189RingHomField · cited by 7404FieldPolynomial · cited by 5681PolynomialPolynomial.X · cited by 1639Polynomial.XMulZeroClass.zero_mul · cited by 1625MulZeroClass.zero_mulPolynomial.C · cited by 1598Polynomial.CPolynomial.natDegree · cited by 1105Polynomial.natDegreePolynomial.map · cited by 806Polynomial.mapPolynomial.eval₂ · cited by 267Polynomial.eval₂AdjoinRoot · cited by 177AdjoinRootAdjoinRoot.root · cited by 77AdjoinRoot.rootAdjoinRoot.of · cited by 52AdjoinRoot.ofPolynomial.eval_map · cited by 37Polynomial.eval_mapPolynomial.IsRoot.def · cited by 30IsRoot.defPolynomial.X_sub_C_mul_remove…CITED BYCITES

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.