Commit 2024-07-16 05:23 d81613c4

View on Github →

chore: remove unused lemmas about bit0/1 (#14707) Deletions:

  • bit0_mul
  • mul_bit0
  • bit1_mul
  • mul_bit1
  • Polynomial.natDegree_bit0
  • Polynomial.natDegree_bit1
  • Polynomial.bit0_comp
  • Polynomial.bit1_comp

Estimated changes

deleted theorem Polynomial.natDegree_bit0
deleted theorem Polynomial.natDegree_bit1