sigma_pos

Mathlib.NumberTheory.ArithmeticFunction

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

English

If n ≠ 0 then 0 < σ_k(n).

Русский

Если n ≠ 0, то 0 < σ_k(n).

LaTeX

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

Lean4

theorem sigma_pos (k n : ℕ) (hn0 : n ≠ 0) : 0 < σ k n := by rwa [sigma_pos_iff, pos_iff_ne_zero]

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

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

Разделы

Аффилиация

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