dvd

Mathlib.Algebra.GroupWithZero.Associated

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

English

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

Русский

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

LaTeX

$$$ [Monoid M] {a b : M} : a ~ᵤ b \rightarrow a \mid b $$$

Lean4

protected theorem dvd [Monoid M] {a b : M} : a ~ᵤ b → a ∣ b := fun ⟨u, hu⟩ => ⟨u, hu.symm⟩

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

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

Разделы

Аффилиация

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