finite_int_prime_iff — Mathlib

English

For a prime p, and integer a, FiniteMultiplicity (p:ℤ) a holds exactly when a ≠ 0.

Русский

Для простого p и целого a: кратность p в a конечна тогда и только тогда, когда a ≠ 0.

LaTeX

$$$\mathrm{FiniteMultiplicity}(p:\mathbb{Z},a) \iff a \neq 0$ (при простой p)$$

Lean4

/-- The multiplicity of `p : ℕ` in `a : ℤ` is finite exactly when `a ≠ 0`. -/
theorem finite_int_prime_iff {a : ℤ} : FiniteMultiplicity (p : ℤ) a ↔ a ≠ 0 := by
  simp [Int.finiteMultiplicity_iff, hp.1.ne_one]

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