Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-12 09:02 fa6c45a8

View on Github →

feat(data/polynomial): simp lemmas for bit0 / bit1 (#3376) Add lemmas on polynomials and bit0/bit1 (as suggested here)

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.C_bit0

added theorem polynomial.C_bit1

added theorem polynomial.eval_bit0

added theorem polynomial.eval_bit1

added theorem polynomial.eval₂_bit0

added theorem polynomial.eval₂_bit1