not_iff_forall — Mathlib

English

¬FiniteMultiplicity a b is equivalent to ∀ n, a^n ∣ b.

Русский

¬FiniteMultiplicity a b эквивалентно ∀ n, a^n ∣ b.

LaTeX

$$$$\neg FiniteMultiplicity\ a\ b \leftrightarrow \forall n : \mathbb{N},\; a^{n} \mid b.$$$$

Lean4

theorem not_iff_forall : ¬FiniteMultiplicity a b ↔ ∀ n : ℕ, a ^ n ∣ b :=
  ⟨fun h n =>
    Nat.casesOn n
      (by
        rw [_root_.pow_zero]
        exact one_dvd _)
      (by simpa [FiniteMultiplicity] using h),
    by simp [FiniteMultiplicity]; tauto⟩

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