Theorems · Definition · number theory

Nat.factorizationLCMRight

ℕ → ℕ → ℕ

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.

Defined in

Mathlib.Data.Nat.Factorization.Defs

Cited by

15 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound