dvd_iff_dvd_right

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associated.dvd_iff_dvd_right

English

If b is associated with c, then a divides b iff a divides c.

Русский

Если b ассоциировано с c, то a делит b тогда и только тогда, когда a делит c.

LaTeX

$$$ [Monoid M] {a b c : M} (h : b ~ᵤ c) : a \mid b \iff a \mid c $$$

Lean4

theorem dvd_iff_dvd_right [Monoid M] {a b c : M} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
  let ⟨_, hu⟩ := h
  hu ▸ Units.dvd_mul_right.symm

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

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

Разделы

Аффилиация

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