Lemmas about factorizationLCMLeft

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

@[simp]

theorem Nat.factorizationLCMLeft_zero_left (b : ℕ) : factorizationLCMLeft 0 b = 1

@[simp]

theorem Nat.factorizationLCMLeft_zero_right (a : ℕ) : a.factorizationLCMLeft 0 = 1

@[simp]

theorem Nat.factorizationLCRight_zero_left (b : ℕ) : factorizationLCMRight 0 b = 1

@[simp]

theorem Nat.factorizationLCMRight_zero_right (a : ℕ) : a.factorizationLCMRight 0 = 1

theorem Nat.factorizationLCMLeft_pos (a b : ℕ) : 0 < a.factorizationLCMLeft b

theorem Nat.factorizationLCMRight_pos (a b : ℕ) : 0 < a.factorizationLCMRight b

theorem Nat.coprime_factorizationLCMLeft_factorizationLCMRight (a b : ℕ) : (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)

theorem Nat.factorizationLCMLeft_mul_factorizationLCMRight {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

theorem Nat.factorizationLCMLeft_dvd_left (a b : ℕ) : a.factorizationLCMLeft b ∣ a

theorem Nat.factorizationLCMRight_dvd_right (a b : ℕ) : a.factorizationLCMRight b ∣ b