Commit 2025-03-11 02:02 6715e25f

View on Github →

chore(Data/Int): address porting notes (#22795) Addresses most porting notes in Data/Int except for those talking about tactics.

Estimated changes

Modified Mathlib/Data/Int/Bitwise.lean

deleted theorem Int.shiftLeft_coe_nat

added theorem Int.shiftLeft_natCast

deleted theorem Int.shiftRight_coe_nat

added theorem Int.shiftRight_natCast

Modified Mathlib/Data/Int/ConditionallyCompleteOrder.lean

Modified Mathlib/Data/Int/Init.lean

Modified Mathlib/Data/Int/Log.lean

modified theorem Int.clog_zpow

modified theorem Int.log_zpow

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/Int/Range.lean