sigma_eq_one_iff — Mathlib

English

σ_k(n) = 1 if and only if n = 1.

Русский

σ_k(n) = 1 тогда и только тогда, когда n = 1.

LaTeX

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

Lean4

@[simp]
theorem sigma_eq_one_iff (k n : ℕ) : σ k n = 1 ↔ n = 1 :=
  by
  by_cases hn0 : n = 0
  · subst hn0
    simp
  constructor
  · intro h
    rw [← sigma_zero_eq_one_iff]
    have zero_lt_sigma := sigma_pos 0 n hn0
    have sigma_zero_le_sigma := sigma_mono 0 k n (Nat.zero_le k)
    cutsat
  · rintro rfl
    simp

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