modEq_zero_iff_dvd

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.modEq_zero_iff_dvd

English

An integer a is congruent to 0 modulo n if and only if n divides a.

Русский

Число a совпадает по модулю n с 0 тогда, когда n делит a.

LaTeX

$$$ a \equiv 0 \,[ZMOD n] \iff n \mid a $$$

Lean4

theorem modEq_zero_iff_dvd : a ≡ 0 [ZMOD n] ↔ n ∣ a := by rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]

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

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

Разделы

Аффилиация

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