base_pow_mul — Mathlib

English

For 1 < p and 0 < n, base_pow_mul yields a relation: p.maxPowDiv(p^exp * n) = p.maxPowDiv(n) + exp.

Русский

Для 1 < p и 0 < n выполняется: 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_pow_mul {p n exp : ℕ} (hp : 1 < p) (hn : 0 < n) : p.maxPowDiv (p ^ exp * n) = p.maxPowDiv n + exp := by
  match exp with
  | 0 => simp
  | e + 1 =>
    rw [Nat.pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm, base_pow_mul hp hn]
    · ac_rfl
    · apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e

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