OAI/Combinatorics/SphericalRamsey/RealTranscendenceBasis.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GrahamSpherical.exists_real_transcendenceBasis_containing line 12

   Source documentation

   The designated transcendental real is retained in the actual maximal algebraically independent subset of the real field.

   theorem exists_real_transcendenceBasis_containing (a : ℝ)
       (ha : Transcendental ℚ a) :
       ∃ B : Set ℝ, a ∈ B ∧ IsTranscendenceBasis ℚ (fun b : B => (b : ℝ)) := by
   …