Theorems · Theorem · field theory
Polynomial.coeff_sub
∀ {R : Type u} [inst : Ring R] (p q : Polynomial R) (n : ℕ), (p - q).coeff n = p.coeff n - q.coeff n- Defined in
- Mathlib.Algebra.Polynomial.Basic
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 91 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.coeproof · cited by 62,936
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- Polynomial.coeffstatement · cited by 1,045
- sub_eq_add_negproof · cited by 1,023
- AddMonoidAlgebra.coeffproof · cited by 365
- Polynomial.toFinsuppproof · cited by 64
- Polynomial.toFinsupp_addproof · cited by 5
- Polynomial.toFinsupp_negproof · cited by 1
Cited by49
Results whose statement or proof uses this declaration.
- IsIntegral.coeffproof · cited by 4
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- Polynomial.resultant_X_sub_C_leftproof · cited by 3
- RatFunc.eq_C_of_minpolyX_coeff_eq_zeroproof · cited by 3
- Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_topproof · cited by 3
- FiniteField.orderOf_frobeniusAlgHomproof · cited by 3
- Polynomial.coeff_hermite_succ_succproof · cited by 3
- X_pow_sub_C_irreducible_of_oddproof · cited by 3
- Matrix.matPolyEquiv_charmatrixproof · cited by 3
- Polynomial.coprime_of_root_cyclotomicproof · cited by 2
- IsLocalization.isAlgebraicproof · cited by 2
- Polynomial.coeff_X_sub_C_mulproof · cited by 2