lcm_eq_normalize — Mathlib

English

If habc: lcm(a,b) | c and hcab: c | lcm(a,b), then lcm(a,b) = normalize(c).

Русский

Если lcm(a,b) делит c и c делит lcm(a,b), то lcm(a,b) равно нормализации c.

LaTeX

$$$ \operatorname{lcm}(a,b) = \operatorname{normalize}(c) \text{ given } (\operatorname{lcm}(a,b) \mid c) \land (c \mid \operatorname{lcm}(a,b)) $$$

Lean4

theorem lcm_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) :
    lcm a b = normalize c :=
  normalize_lcm a b ▸ normalize_eq_normalize habc hcab

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