Theorems · Theorem · field theory
Polynomial.eval_ofNat
∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo] (a : R),
Polynomial.eval a (OfNat.ofNat n) = OfNat.ofNat n- Defined in
- Mathlib.Algebra.Polynomial.Eval.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringNat.AtLeastTwo
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 5,681
- Polynomial.evalstatement · cited by 796
- Nat.AtLeastTwostatement and proof · cited by 405
- Polynomial.eval_natCastproof · cited by 24
Cited by18
Results whose statement or proof uses this declaration.
- Polynomial.Chebyshev.T_eval_negproof · cited by 4
- Polynomial.Chebyshev.U_complex_cosproof · cited by 3
- Polynomial.Chebyshev.T_complex_cosproof · cited by 3
- Polynomial.Chebyshev.T_eval_oneproof · cited by 3
- Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_evalproof · cited by 2
- Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_evalproof · cited by 2
- Polynomial.Chebyshev.U_eval_oneproof · cited by 2
- Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureTproof · cited by 2
- Polynomial.Chebyshev.U_eval_zeroproof · cited by 2
- Polynomial.Chebyshev.T_eval_zeroproof · cited by 2
- Polynomial.Chebyshev.C_two_mul_complex_cosproof · cited by 1
- Polynomial.Chebyshev.C_two_mul_complex_coshproof · cited by 1