Descent of rational linear systems

A rational linear system which has a real solution also has a rational solution. The proof applies a rational-linear projection from the reals onto the rationals.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_ratLinear_one : ∃ (p : ℝ →ₗ[ℚ] ℚ), p 1 = 1

A rational-linear functional on the reals taking 1 to 1.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_ratLinear_retraction : ∃ (p : ℝ →ₗ[ℚ] ℚ), ∀ (q : ℚ), p ↑q = q

A rational-linear projection from the reals to the rationals.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_rat_solution_of_real {I : Type u_1} {J : Type u_2} [Fintype I] (A : I → J → ℚ) (b : J → ℚ) (h : ∃ (x : I → ℝ), ∀ (j : J), ∑ i : I, x i * ↑(A i j) = ↑(b j)) : ∃ (q : I → ℚ), ∀ (j : J), ∑ i : I, q i * A i j = b j

Solvability of a finite rational linear system descends from real to rational coefficients. The set of equations need not be finite.