Theorems · Theorem · field theory
Polynomial.natDegree_sub_C
∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {a : R}, (p - Polynomial.C a).natDegree = p.natDegree- Cited by
- 24 results in Mathlib
- Foundations
- Depth 105 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.
Cites9
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.Cstatement and proof · cited by 1,598
- Polynomial.natDegreestatement and proof · cited by 1,105
- sub_eq_add_negproof · cited by 1,023
- Polynomial.C_negproof · cited by 25
- Polynomial.natDegree_add_Cproof · cited by 18
Cited by24
Results whose statement or proof uses this declaration.
- Polynomial.natDegree_X_sub_Cproof · cited by 22
- Polynomial.natDegree_multiset_prod_X_sub_C_eq_cardproof · cited by 6
- natDegree_minpolyDiv_succproof · cited by 4
- X_pow_sub_C_irreducible_of_oddproof · cited by 3
- Polynomial.resultant_X_sub_C_leftproof · cited by 3
- IsPurelyInseparable.elemExponent_le_of_pow_memproof · cited by 3
- IsPurelyInseparable.minpoly_natDegree_eqproof · cited by 2
- Polynomial.resultant_X_sub_C_pow_leftproof · cited by 2
- IsRealClosed.exists_eq_pow_of_oddproof · cited by 2
- Polynomial.Monic.exists_splits_mapproof · cited by 2
- IsPurelyInseparable.finrank_eq_powproof · cited by 2
- Polynomial.X_sub_C_scaleRootsproof · cited by 1