Theorems · Theorem · field theory
Polynomial.leadingCoeff_X_sub_C
∀ {S : Type v} [inst : Ring S] (r : S), (Polynomial.X - Polynomial.C r).leadingCoeff = 1- Cited by
- 11 results in Mathlib
- Foundations
- Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- RingHomstatement · cited by 10,189
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- Polynomial.Xstatement and proof · cited by 1,639
- Polynomial.Cstatement and proof · cited by 1,598
- sub_eq_add_negproof · cited by 1,023
- Polynomial.leadingCoeffstatement and proof · cited by 498
- map_negproof · cited by 378
- Polynomial.leadingCoeff_X_add_Cproof · cited by 5
Cited by11
Results whose statement or proof uses this declaration.
- natDegree_minpolyDiv_succproof · cited by 4
- Polynomial.coeff_preHilbertPoly_selfproof · cited by 2
- Polynomial.resultant_X_sub_C_pow_leftproof · cited by 2
- Polynomial.succ_signVariations_le_X_sub_C_mulproof · cited by 1
- minpolyDiv_monicproof · cited by 1
- Polynomial.rootMultiplicity_scaleRootsproof · cited by 1
- monic_descPochhammerproof · cited by 1
- Polynomial.Splits.eq_X_sub_C_of_single_rootproof · cited by 1
- Polynomial.splits_X_sub_C_mul_iffproof · cited by 1
- Polynomial.succ_signVariations_X_sub_C_mul_monomialproof · cited by 0
- Polynomial.cauchyBound_X_sub_Cproof · cited by 0