Parity of natural numbers #
This file contains theorems about the Even
and Odd
predicates on the natural numbers.
Tags #
even, odd
theorem
Function.Involutive.iterate_bit0
{α : Type u_1}
{f : α → α}
(hf : Function.Involutive f)
(n : ℕ)
:
theorem
Function.Involutive.iterate_bit1
{α : Type u_1}
{f : α → α}
(hf : Function.Involutive f)
(n : ℕ)
:
theorem
Function.Involutive.iterate_two_mul
{α : Type u_1}
{f : α → α}
(hf : Function.Involutive f)
(n : ℕ)
:
theorem
Function.Involutive.iterate_even
{α : Type u_1}
{f : α → α}
{n : ℕ}
(hf : Function.Involutive f)
(hn : Even n)
:
theorem
Function.Involutive.iterate_odd
{α : Type u_1}
{f : α → α}
{n : ℕ}
(hf : Function.Involutive f)
(hn : Odd n)
: