isDivSequence_id

Mathlib.NumberTheory.EllipticDivisibilitySequence

URI: https://scilib.ai/kg/mathlib#isDivSequence_id

English

The identity sequence id is a divisibility sequence: for all m,n ∈ ℕ, if m divides n then m divides n.

Русский

Идентичная последовательность id является последовательностью делимости: для любых m,n ∈ ℕ, если m делит n, то m делит n.

LaTeX

$$$ IsDivSequence(id) $$$

Lean4

theorem isDivSequence_id : IsDivSequence id := fun _ _ => Int.ofNat_dvd.mpr

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

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

Разделы

Аффилиация

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