RationalSpan.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.exists_ratLinear_one line 17
Source documentation
A rational-linear functional on the reals taking 1 to 1.
```
theorem exists_ratLinear_one :
    ∃ p : ℝ →ₗ[ℚ] ℚ, p 1 = 1 :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_ratLinear_retraction line 22
Source documentation
A rational-linear projection from the reals to the rationals.
```
theorem exists_ratLinear_retraction :
    ∃ p : ℝ →ₗ[ℚ] ℚ, ∀ q : ℚ, p (q : ℝ) = q := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_rat_solution_of_real line 31

Source documentation

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

theorem exists_rat_solution_of_real {I : Type*} {J : Type*} [Fintype I]
    (A : I → J → ℚ) (b : J → ℚ)
    (h : ∃ x : I → ℝ, ∀ j, ∑ i, x i * (A i j : ℝ) = (b j : ℝ)) :
    ∃ q : I → ℚ, ∀ j, ∑ i, q i * A i j = b j := by
…