gcd_mul_lcm

Mathlib.Algebra.GCDMonoid.Basic

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

English

For any a,b in a gcd-monoid α, gcd(a,b)·lcm(a,b) is associated to a·b.

Русский

Для любых a,b в gcd-монойде α произведение gcd(a,b) и lcm(a,b) ассоциировано с произведением a·b.

LaTeX

$$$$ \\operatorname{Associated}(\\gcd(a,b) \\cdot \\operatorname{lcm}(a,b), a \\cdot b) $$$$

Lean4

theorem gcd_mul_lcm [GCDMonoid α] : ∀ a b : α, Associated (gcd a b * lcm a b) (a * b) :=
  GCDMonoid.gcd_mul_lcm

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

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

Разделы

Аффилиация

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