Commit 2024-06-14 08:25 c07d9885

View on Github →

chore(*): drop some bit0/bit1 lemmata (#13822)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

deleted theorem Polynomial.C_bit0

deleted theorem Polynomial.C_bit1

Modified Mathlib/Algebra/Polynomial/Coeff.lean

deleted theorem Polynomial.coeff_bit0

deleted theorem Polynomial.coeff_bit0_mul

deleted theorem Polynomial.coeff_bit1_mul

Modified Mathlib/Algebra/Polynomial/Eval.lean

deleted theorem Polynomial.eval_bit0

deleted theorem Polynomial.eval_bit1

deleted theorem Polynomial.eval₂_bit0

deleted theorem Polynomial.eval₂_bit1

Modified Mathlib/Probability/Variance.lean