Commit 2023-03-08 08:35 31ab272b

View on Github →

feat: Port Data.Polynomial.Induction (#2628) Mostly just rename.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Induction.lean

added theorem Polynomial.exists_C_coeff_not_mem

added theorem Polynomial.mem_span_C_coeff

added theorem Polynomial.span_le_of_C_coeff_mem