Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-28 01:14
76badb27
View on Github →
chore: deprecate Function.Involutive.iterate_bit{0,1} (
#30986
)
Estimated changes
Modified
Mathlib/Algebra/Ring/Parity.lean
deleted
theorem
Function.Involutive.iterate_bit0
deleted
theorem
Function.Involutive.iterate_bit1
added
theorem
Function.Involutive.iterate_two_mul_add_one