dvd_dvd

Mathlib.Algebra.GroupWithZero.Associated

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

English

If a is associated with b, then a divides b and b divides a.

Русский

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

LaTeX

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

Lean4

protected theorem dvd_dvd [Monoid M] {a b : M} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
  ⟨h.dvd, h.symm.dvd⟩

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

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

Разделы

Аффилиация

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