Documentation

Collatz.Basic

source
@[simp]
theorem Collatz.collatz_even {n : ℕ} (h : n % 2 = 0) :
collatz n = n / 2
source
@[simp]
theorem Collatz.collatz_odd {n : ℕ} (h : n % 2 = 1) :
collatz n = 3 * n + 1
source
@[simp]
theorem Collatz.collatz_zero :
collatz 0 = 0
source
@[simp]
theorem Collatz.collatz_one :
collatz 1 = 4
source
@[simp]
theorem Collatz.collatz_two :
collatz 2 = 1
source
@[simp]
theorem Collatz.collatz_four :
collatz 4 = 2
source
theorem Collatz.collatz_odd_is_even {n : ℕ} (h : n % 2 = 1) :
collatz n % 2 = 0