Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-12 05:04 15b5e24e

View on Github →

feat(data/polynomial/taylor): taylor's formula (#11139) Via proofs about hasse_deriv. Added some monomial API too.

Estimated changes

Modified src/data/finset/lattice.lean

added theorem finset.sup_ite

Modified src/data/nat/with_bot.lean

added theorem nat.with_bot.lt_one_iff_le_zero

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.degree_C_lt

added theorem polynomial.leading_coeff_pow_X_add_C

Modified src/data/polynomial/hasse_deriv.lean

added theorem polynomial.hasse_deriv_eq_zero_of_lt_nat_degree

added theorem polynomial.nat_degree_hasse_deriv

added theorem polynomial.nat_degree_hasse_deriv_le

Modified src/data/polynomial/taylor.lean

added theorem polynomial.nat_degree_taylor

added theorem polynomial.sum_taylor_eq

added theorem polynomial.taylor_monomial

added theorem polynomial.taylor_taylor

added theorem polynomial.taylor_zero'

added theorem polynomial.taylor_zero