instCommutativeLcm

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#instCommutativeLcm

English

In NormalizedGCDMonoid α, the lcm operation is commutative as a standard operation: lcm is commutative.

Русский

В нормализованном gcd-монойде НОК является коммутативной операцией: lcm(a,b) = lcm(b,a).

LaTeX

$$$ \operatorname{lcm} \text{ is commutative on } \alpha $$$

Lean4

instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) lcm where comm := lcm_comm

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

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

Разделы

Аффилиация

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