ne_zero_of_mem_smoothNumbers

Mathlib.NumberTheory.SmoothNumbers

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

English

No zero is a smooth number: every smooth number is nonzero.

Русский

Ноль не является гладным числом: каждое гладкое число ненулево.

LaTeX

$$$\forall n, \ m \in n.\mathrm{smoothNumbers} \Rightarrow m \neq 0$$$

Lean4

/-- Zero is never a smooth number -/
theorem ne_zero_of_mem_smoothNumbers {n m : ℕ} (h : m ∈ smoothNumbers n) : m ≠ 0 :=
  h.1

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

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

Разделы

Аффилиация

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