Clearing denominators in nonnegative rational families

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nat_eq_mul_rat_of_den_dvd {q : ℚ} (hq : 0 ≤ q) {D : ℕ} (hD : q.den ∣ D) : ∃ (c : ℕ), ↑D * q = ↑c

Every natural multiple of a denominator clears its nonnegative rational.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nat_mul_eq_nat {I : Type u_1} [Finite I] (q : I → ℚ) (hq : ∀ (i : I), 0 ≤ q i) : ∃ (D : ℕ), 0 < D ∧ ∃ (c : I → ℕ), ∀ (i : I), ↑D * q i = ↑(c i)

A finite nonnegative rational family has a common positive denominator which turns every coefficient into a natural number.