pos_of_mem_divisors

Mathlib.NumberTheory.Divisors

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

← MathLib Explorer

English

If m is in divisors n, then m > 0.

Русский

Если m принадлежит divisors(n), то m > 0.

LaTeX

$$$m\\in \\mathrm{divisors}(n) \\Rightarrow 0 < m$$$

Lean4

theorem pos_of_mem_divisors {m : ℕ} (h : m ∈ n.divisors) : 0 < m :=
  by
  cases m
  · rw [mem_divisors, zero_dvd_iff (a := n)] at h
    cases h.2 h.1
  apply Nat.succ_pos

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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