finiteMultiplicity_mul — Mathlib

English

If p is prime and a, b have finite p-multiplicity, then a · b has finite p-multiplicity.

Русский

Пусть p — простое число, и у a, b конечная p-кратность; тогда произведение a·b имеет конечную p-кратность.

LaTeX

$$$ \forall {a,b} (hp : Prime p) , FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a b)$$$

Lean4

theorem finiteMultiplicity_mul {p a b : α} (hp : Prime p) :
    FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a * b) := fun ⟨n, hn⟩ ⟨m, hm⟩ =>
  ⟨n + m, finiteMultiplicity_mul_aux hp hn hm⟩

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