Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-09 09:07 42813431

View on Github →

refactor(data/polynomial): redefine C as an alg_hom (#3003) As a side effect Lean parses C 1 as polynomial nat. If you need polynomial R, then use C (1:R).

Estimated changes

modified def polynomial.C
modified theorem polynomial.C_0
modified theorem polynomial.C_1
modified theorem polynomial.C_add
added theorem polynomial.C_def
modified theorem polynomial.C_mul
modified theorem polynomial.C_neg
modified theorem polynomial.C_pow
modified theorem polynomial.C_sub
modified theorem polynomial.int_cast_eq_C
modified def polynomial.lcoeff
modified theorem polynomial.nat_cast_eq_C