OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Convex/RationalDenominators.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nat_eq_mul_rat_of_den_dvd line 14

   Source documentation

   Every natural multiple of a denominator clears its nonnegative rational.

   theorem exists_nat_eq_mul_rat_of_den_dvd {q : ℚ} (hq : 0 ≤ q)
       {D : ℕ} (hD : q.den ∣ D) :
       ∃ c : ℕ, (D : ℚ) * q = (c : ℚ) := by
   …

2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nat_mul_eq_nat line 29

   Source documentation

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

   theorem exists_nat_mul_eq_nat {I : Type*} [Fintype I]
       (q : I → ℚ) (hq : ∀ i, 0 ≤ q i) :
       ∃ D : ℕ, 0 < D ∧ ∃ c : I → ℕ, ∀ i, (D : ℚ) * q i = (c i : ℚ) := by
   …