base_mul_eq_succ — Mathlib

English

If p > 1 and n > 0, then p.maxPowDiv(p^exp * n) = p.maxPowDiv(n) + exp.

Русский

Если p > 1 и n > 0, то p.maxPowDiv(p^exp · n) = p.maxPowDiv(n) + exp.

LaTeX

$$$ (1 < p) \\land (0 < n) \\implies p.maxPowDiv(p^{\\text{exp}} \\cdot n) = p.maxPowDiv(n) + \\text{exp} $$$

Lean4

theorem base_mul_eq_succ {p n : ℕ} (hp : 1 < p) (hn : 0 < n) : p.maxPowDiv (p * n) = p.maxPowDiv n + 1 :=
  by
  have : 0 < p := lt_trans (b := 1) (by simp) hp
  dsimp [maxPowDiv]
  rw [maxPowDiv.go, if_pos, mul_div_right _ this]
  · apply go_succ
  · refine ⟨hp, ?_, by simp⟩
    apply Nat.mul_pos this hn

Похожие утверждения