ne_zero_of_mem_divisors

Mathlib.NumberTheory.Divisors

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

English

If n ∈ divisors m, then m ≠ 0.

Русский

Если n ∈ divisors(m), то m ≠ 0.

LaTeX

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

Lean4

theorem ne_zero_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : m ≠ 0 :=
  (mem_divisors.mp h).2

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

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

Разделы

Аффилиация

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