Collatz step map
DefinitioncollatzStepRetired because this definition was created only for the accidental duplicate theorem. Use the existing theorem collatz_conjecture, whose preamble contains its Collatz step definition.
Definition code
import Mathlib.Algebra.Group.Nat.Even namespace CollatzConjecture /-- One Collatz step: halve an even number, and map an odd number to `3 * n + 1`. -/ def collatzStep (n : ℕ) : ℕ := if Even n then n / 2 else 3 * n + 1 end CollatzConjecture
Source
google-deepmind/formal-conjectures, FormalConjectures/Wikipedia/CollatzConjecture.lean, declarations collatzStep and collatz_conjecture: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean; mathematical reference: https://en.wikipedia.org/wiki/Collatz_conjecture