Commit 2024-06-18 08:57 bb955cd6

View on Github →

chore(*): drop bit*_mono (#13914)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

deleted theorem bit0_pos

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

deleted theorem bit0_mono

deleted theorem bit0_strictMono

Modified Mathlib/Algebra/Order/Ring/Defs.lean

deleted theorem bit0_le_bit0

deleted theorem bit0_lt_bit0

deleted theorem bit1_le_bit1

deleted theorem bit1_lt_bit1

deleted theorem bit1_mono

deleted theorem bit1_pos'

deleted theorem bit1_pos

deleted theorem one_le_bit1

deleted theorem one_lt_bit1

deleted theorem zero_le_bit0

deleted theorem zero_lt_bit0

Modified Mathlib/Data/Num/Prime.lean