Documentation

Mathlib.Data.Nat.Factorization.LCM

Lemmas about factorizationLCMLeft #

This file contains some lemmas about factorizationLCMLeft. These were split from Mathlib.Data.Nat.Factorization.Basic to reduce transitive imports.