English
For natural numbers a,b, FiniteMultiplicity a b holds exactly when a ≠ 1 and 0 < b.
Русский
Для натуральных чисел a,b верно: FiniteMultiplicity a b тогда и только тогда, когда a ≠ 1 и 0 < b.
LaTeX
$$$\operatorname{FiniteMultiplicity}(a,b) \iff a \neq 1 \land 0 < b$$$
Lean4
theorem finiteMultiplicity_iff {a b : ℕ} : FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b :=
by
rw [← not_iff_not, FiniteMultiplicity.not_iff_forall, not_and_or, not_ne_iff, not_lt, Nat.le_zero]
exact
⟨fun h =>
or_iff_not_imp_right.2 fun hb =>
have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
Classical.by_contradiction fun ha1 : a ≠ 1 =>
have ha_gt_one : 1 < a :=
lt_of_not_ge fun _ =>
match a with
| 0 => ha rfl
| 1 => ha1 rfl
| b + 2 => by cutsat
not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (b.lt_pow_self ha_gt_one),
fun h => by cases h <;> simp [*]⟩
