pos_of_div_pos

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.pos_of_div_pos

← MathLib Explorer

English

If a divides n and n is positive, then a is positive.

Русский

Если a делит n и n положительно, то a положительно.

LaTeX

$$$ \\forall n \\in \\mathbb{N}^+, \\forall a \\in \\mathbb{N},\\; a \\mid n \\Rightarrow 0 < a.$$$

Lean4

theorem pos_of_div_pos {n : ℕ+} {a : ℕ} (h : a ∣ n) : 0 < a :=
  by
  apply pos_iff_ne_zero.2
  intro hzero
  rw [hzero] at h
  exact PNat.ne_zero n (eq_zero_of_zero_dvd h)

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

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

Разделы

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

Аффилиация

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