finiteMultiplicity_iff_finiteMultiplicity_natAbs

English

Finite multiplicity for integers corresponds to finite multiplicity of their absolute values.

Русский

Конечная кратность для целых чисел эквивалентна конечной кратности их модулей.

LaTeX

$$$ FiniteMultiplicity a b \leftrightarrow FiniteMultiplicity a.{natAbs} b.{natAbs} $$$

Lean4

theorem finiteMultiplicity_iff_finiteMultiplicity_natAbs {a b : ℤ} :
    FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs := by
  simp only [FiniteMultiplicity.def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]

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