English
Define factorizationLCMRight(a,b) as the product over primes of p^n with n = m_i when n_i < m_i, otherwise 0.
Русский
Определяем factorizationLCMRight(a,b) как произведение по простым p^n, где n = m_i если n_i < m_i, иначе 0.
LaTeX
$$$\\operatorname{factorizationLCMRight}(a,b) = (\\operatorname{lcm}(a,b)).factorization.\\mathrm{prod}\\; (p\\, n \\mapsto \\text{if } b.factorization(p) ≤ a.factorization(p) \\text then } 1 \\text{ else } p^n$$$
Lean4
/-- If `a = ∏ pᵢ ^ nᵢ` and `b = ∏ pᵢ ^ mᵢ`, then `factorizationLCMRight = ∏ pᵢ ^ kᵢ`, where
`kᵢ = mᵢ` if `nᵢ < mᵢ` 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`.
Note that `factorizationLCMRight a b` is *not* `factorizationLCMLeft b a`: the difference is
that in `factorizationLCMLeft a b` there are the primes whose exponent in `a` is bigger or equal
than the exponent in `b`, while in `factorizationLCMRight a b` there are the primes whose
exponent in `b` is strictly bigger than in `a`. For example `factorizationLCMLeft 2 2 = 2`, but
`factorizationLCMRight 2 2 = 1`. -/
def factorizationLCMRight (a b : ℕ) :=
(Nat.lcm a b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n
