finiteMultiplicity_iff — Mathlib

English

For integers a,b, FiniteMultiplicity a b is equivalent to a.natAbs ≠ 1 and b ≠ 0.

Русский

Для целых чисел a,b эквивалентно FiniteMultiplicity a b ≡ (a.natAbs ≠ 1 ∧ b ≠ 0).

LaTeX

$$$ \forall a,b : \mathbb{Z}, FiniteMultiplicity a b \leftrightarrow a.natAbs \neq 1 \land b \neq 0 $$$

Lean4

theorem finiteMultiplicity_iff {a b : ℤ} : FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0 := by
  rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff, pos_iff_ne_zero, Int.natAbs_ne_zero]

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