normalize_lcm — Mathlib

English

In a NormalizedGCDMonoid, the lcm is already in normalized form, i.e., normalize(lcm(a,b)) = lcm(a,b).

Русский

В нормализованном gcd-монойде НОК уже нормализована: normalize(lcm(a,b)) = lcm(a,b).

LaTeX

$$$ \operatorname{normalize}(\operatorname{lcm}(a,b)) = \operatorname{lcm}(a,b) $$$

Lean4

@[simp]
theorem normalize_lcm [NormalizedGCDMonoid α] (a b : α) : normalize (lcm a b) = lcm a b :=
  NormalizedGCDMonoid.normalize_lcm a b

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