Theorems · Theorem · field theory
Polynomial.coeff_zero_eq_eval_zero
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.coeff 0 = Polynomial.eval 0 p- Defined in
- Mathlib.Algebra.Polynomial.Eval.Coeff
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Polynomialstatement and proof · cited by 5,681
- mul_oneproof · cited by 3,885
- MulZeroClass.mul_zeroproof · cited by 2,091
- pow_zeroproof · cited by 1,094
- Polynomial.coeffstatement and proof · cited by 1,045
- Polynomial.evalstatement · cited by 796
- MonoidWithZeroproof · cited by 456
- zero_powproof · cited by 361
- Polynomial.supportproof · cited by 237
- Finset.sum_eq_singleproof · cited by 98
- Polynomial.eval_eq_sumproof · cited by 8
Cited by20
Results whose statement or proof uses this declaration.
- Matrix.det_eq_sign_charpoly_coeffproof · cited by 5
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- Polynomial.bernoulli_eval_zeroproof · cited by 3
- Polynomial.coprime_of_root_cyclotomicproof · cited by 2
- Polynomial.zero_isRoot_iff_coeff_zero_eq_zeroproof · cited by 2
- Polynomial.coeff_zero_eq_aeval_zeroproof · cited by 2
- LinearMap.hasEigenvalue_zero_tfaeproof · cited by 2
- Polynomial.irreducible_of_eisenstein_criterionproof · cited by 1
- Polynomial.eval_divByMonic_eq_trailingCoeff_compproof · cited by 1
- Matrix.det_one_add_X_smulproof · cited by 1
- cyclotomic_comp_X_add_one_isEisensteinAtproof · cited by 1
- cyclotomic_prime_pow_comp_X_add_one_isEisensteinAtproof · cited by 1