dvd_iff_dvd_of_dvd_sub

Mathlib.Algebra.Ring.Divisibility.Basic

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

English

For a and b, a | (b−c) ⇔ a|b under the right conditions.

Русский

Для a и b, a|(b−c) ⇔ a|b при соответствующих условиях.

LaTeX

$$$a \mid (b - c) \iff a \mid b$$$

Lean4

theorem dvd_iff_dvd_of_dvd_sub (h : a ∣ b - c) : a ∣ b ↔ a ∣ c := by rw [← sub_add_cancel b c, dvd_add_right h]

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

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

Разделы

Аффилиация

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