Commit 2024-07-12 11:12 e0d8b5b4

View on Github →

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

Estimated changes

Modified Mathlib/Data/Int/Defs.lean

deleted theorem Int.ofNat_bit0

deleted theorem Int.ofNat_bit1

Modified Mathlib/LinearAlgebra/Matrix/ZPow.lean

deleted theorem Matrix.zpow_bit0'

deleted theorem Matrix.zpow_bit0

deleted theorem Matrix.zpow_bit1'

deleted theorem Matrix.zpow_bit1