Lemma: MrTheorem18_Collatz_1c53d8a4.iterate_power_two_mul

For all natural r and n, the imported Collatz map sends 2^r*n to n after r steps. This is repeated halving, not convergence for arbitrary n.

Exact formal statement

∀ (r n : Nat),
  Eq.{1}
    (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep r (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 r) n))
    n

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.