dvd_sub_comm

Mathlib.Algebra.Ring.Divisibility.Basic

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

English

a | b−c ⇔ a | c−b.

Русский

a делит b−c ⇔ a делит c−b.

LaTeX

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

Lean4

theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg, neg_sub]

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

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

Разделы

Аффилиация

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