pos_of_mem_properDivisors

Mathlib.NumberTheory.Divisors

URI: https://scilib.ai/kg/mathlib#Nat.pos_of_mem_properDivisors

English

If m ∈ n.properDivisors, then m > 0.

Русский

Если m ∈ n.properDivisors, то m > 0.

LaTeX

$$$m\\in n.properDivisors \\Rightarrow 0 < m$$$

Lean4

theorem pos_of_mem_properDivisors {m : ℕ} (h : m ∈ n.properDivisors) : 0 < m :=
  pos_of_mem_divisors (properDivisors_subset_divisors h)

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

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

Разделы

Аффилиация

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