Nat.maxPowDiv.go_eq

theorem Nat.maxPowDiv.go_eq : ∀ {k p n : ℕ}, Nat.maxPowDiv.go k p n = if 1 < p ∧ 0 < n ∧ n % p = 0 then Nat.maxPowDiv.go (k + 1) p (n / p) else k

The theorem `Nat.maxPowDiv.go_eq` states that for any natural numbers `k`, `p`, and `n`, the function `Nat.maxPowDiv.go` applied to `k`, `p`, and `n` equals `k` if `p` is less than or equal to 1, or `n` is zero, or `n` is not divisible by `p`. However, if `p` is greater than 1, `n` is positive and `n` is divisible by `p`, the function `Nat.maxPowDiv.go` equals the result of recursively calling the function itself but with `k + 1` and `n` divided by `p`. In other words, this function recursively divides `n` by `p` and increments `k` as long as `n` is divisible by `p` and `p` is greater than 1.

More concisely: The theorem `Nat.maxPowDiv.go_eq` states that `Nat.maxPowDiv.go k p n = k` if `p <= 1` or `n = 0` or `n mod p /= 0`, and otherwise `Nat.maxPowDiv.go (k + 1) (n // p)`.