sigma_eq_zero — Mathlib

English

For all k and n, σ_k(n) = 0 if and only if n = 0.

Русский

Для всех k и n верно: σ_k(n) = 0 тогда и только тогда, когда n = 0.

LaTeX

$$$ \sigma_k(n) = 0 \iff n = 0 $$$

Lean4

@[simp]
theorem sigma_eq_zero {k n : ℕ} : σ k n = 0 ↔ n = 0 :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · refine iff_of_false ?_ hn
    simp_rw [ArithmeticFunction.sigma_apply, Finset.sum_eq_zero_iff, not_forall]
    use 1
    simp [hn]

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