dvd'

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associated.dvd'

English

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

Русский

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

LaTeX

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

Lean4

protected theorem dvd' [Monoid M] {a b : M} (h : a ~ᵤ b) : b ∣ a :=
  h.symm.dvd

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

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

Разделы

Аффилиация

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