Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Collatz step

Conjectura.Defs.Mathematics.NumberTheory.CollatzStep

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Nat.Notation

/-! # Collatz step -/

namespace Conjectura.NumberTheory

/-- One **Collatz step**: halve an even number, or triple an odd one and add one. -/
def collatzStep (n : ℕ) : ℕ := if n % 2 = 0 then n / 2 else 3 * n + 1

end Conjectura.NumberTheory