dvd_iff_dvd_left

Mathlib.Algebra.GroupWithZero.Associated

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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