Lemmas about factorizationLCMLeft
#
This file contains some lemmas about factorizationLCMLeft
.
These were split from Mathlib.Data.Nat.Factorization.Basic
to reduce transitive imports.
theorem
Nat.coprime_factorizationLCMLeft_factorizationLCMRight
(a b : ℕ)
:
(a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)