factorizationLCMLeft_mul_factorizationLCMRight

English

The product of the left and right factorizations equals the full LCM factorization of a and b.

Русский

Произведение левой и правой факторизаций даёт полную факторизацию НОК.

LaTeX

$$$(\text{factorizationLCMLeft }a b) \cdot (\text{factorizationLCMRight }a b) = \operatorname{lcm}(a,b).$$$

Lean4

theorem factorizationLCMLeft_mul_factorizationLCMRight (ha : a ≠ 0) (hb : b ≠ 0) :
    (factorizationLCMLeft a b) * (factorizationLCMRight a b) = lcm a b :=
  by
  rw [← factorization_prod_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft, factorizationLCMRight, ← prod_mul]
  congr; ext p n; split_ifs <;> simp

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