English
Define factorizationLCMLeft(a,b) as the product over primes of p^n with n = a.factorization(p) if b.factorization(p) ≤ a.factorization(p), else n = 0.
Русский
Определяем factorizationLCMLeft(a,b) как произведение по простым p^n, где n = a.factorization(p) если b.factorization(p) ≤ a.factorization(p), иначе n = 0.
LaTeX
$$$\\operatorname{factorizationLCMLeft}(a,b) = (\\operatorname{lcm}(a,b)).factorization.\\mathrm{prod}\\; (p\\, n \\mapsto \\text{if } b.factorization(p) ≤ a.factorization(p) \\text{ then } p^n \\text{ else } 1)$$$
Lean4
/-- If `a = ∏ pᵢ ^ nᵢ` and `b = ∏ pᵢ ^ mᵢ`, then `factorizationLCMLeft = ∏ pᵢ ^ kᵢ`, where
`kᵢ = nᵢ` if `mᵢ ≤ nᵢ` and `0` otherwise. Note that the product is over the divisors of `lcm a b`,
so if one of `a` or `b` is `0` then the result is `1`. -/
def factorizationLCMLeft (a b : ℕ) : ℕ :=
(Nat.lcm a b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1
