nonempty_divisors

Mathlib.NumberTheory.Divisors

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

English

(divisors n) is Nonempty iff n ≠ 0.

Русский

(divisors n) ненулево тогда и только тогда, когда n ≠ 0.

LaTeX

$$$( \\mathrm{divisors}(n) ).\\text{Nonempty} \\Leftrightarrow n \\neq 0$$$

Lean4

@[simp]
theorem nonempty_divisors : (divisors n).Nonempty ↔ n ≠ 0 :=
  ⟨fun ⟨m, hm⟩ hn ↦ by simp [hn] at hm, fun hn ↦ ⟨1, one_mem_divisors.2 hn⟩⟩

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

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

Разделы

Аффилиация

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