Theorems · Theorem · field theory
Polynomial.derivative_sub
∀ {R : Type u} [inst : Ring R] {f g : Polynomial R},
Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g- Defined in
- Mathlib.Algebra.Polynomial.Derivative
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 106 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- map_subproof · cited by 565
- Polynomial.derivativestatement and proof · cited by 331
Cited by22
Results whose statement or proof uses this declaration.
- Polynomial.Chebyshev.T_derivative_eq_Uproof · cited by 7
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- Polynomial.iterate_derivative_comp_one_sub_Xproof · cited by 3
- Polynomial.derivative_X_sub_Cproof · cited by 3
- FiniteField.roots_X_pow_card_sub_Xproof · cited by 2
- galois_poly_separableproof · cited by 1
- Lagrange.derivative_nodalproof · cited by 1
- exists_derivative_mul_eq_and_isIntegral_coeffproof · cited by 1
- WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zeroproof · cited by 1