sigma_pos_iff

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.sigma_pos_iff

English

If n ≠ 0 then 0 < σ_k(n) for all k.

Русский

Если n ≠ 0, то для любого k выполняется 0 < σ_k(n).

LaTeX

$$$ n \neq 0 \Rightarrow 0 < \sigma_k(n) $$$

Lean4

@[simp]
theorem sigma_pos_iff {k n} : 0 < σ k n ↔ 0 < n := by simp [pos_iff_ne_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru