Commit 2024-07-12 03:46 79b532cf

View on Github →

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

Estimated changes

Modified Mathlib/Data/Int/Cast/Basic.lean

deleted theorem Int.cast_bit0

deleted theorem Int.cast_bit1

Modified Mathlib/Data/Matrix/Basic.lean

deleted theorem Matrix.bit0_apply

deleted theorem Matrix.bit1_apply

deleted theorem Matrix.bit1_apply_eq

deleted theorem Matrix.bit1_apply_ne

Modified Mathlib/Data/Rat/Cast/CharZero.lean

deleted theorem Rat.cast_bit0

deleted theorem Rat.cast_bit1

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

deleted theorem MvPolynomial.coe_bit0

deleted theorem MvPolynomial.coe_bit1

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

deleted theorem Polynomial.coe_bit0

deleted theorem Polynomial.coe_bit1

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.lift_bit0

deleted theorem Cardinal.lift_bit1

deleted theorem Cardinal.power_bit0

deleted theorem Cardinal.power_bit1