Theorem Function.Involutive.iterate_two_mul_add_one

Modification history

2025-10-28 01:14
Mathlib/Algebra/Ring/Parity.lean
chore: deprecate Function.Involutive.iterate_bit{0,1} (#30986)
Added Function.Involutive.iterate_two_mul_add_oneView on Github →