mem_divisors_self

Mathlib.NumberTheory.Divisors

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

English

For any n ≠ 0, n ∈ n.divisors.

Русский

Для любого n ≠ 0, n принадлежит n.divisors.

LaTeX

$$$(n : \mathbb{N}) \ (n \neq 0) \Rightarrow n \in n.divisors$$$

Lean4

theorem mem_divisors_self (n : ℕ) (h : n ≠ 0) : n ∈ n.divisors :=
  mem_divisors.2 ⟨dvd_rfl, h⟩

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

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

Разделы

Аффилиация

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