OAI/Combinatorics/SphericalRamsey/BasisDerivation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GrahamSpherical.Poly line 14
  2. abbrev OAI.GrahamSpherical.RatFun line 15
  3. def OAI.GrahamSpherical.tangentCoefficient line 17
  4. def OAI.GrahamSpherical.tangentVariable line 21
  5. def OAI.GrahamSpherical.polynomialTangent line 27
  6. theorem OAI.GrahamSpherical.polynomialTangent_X line 31
  7. theorem OAI.GrahamSpherical.polynomialTangent_fst line 35
  8. theorem OAI.GrahamSpherical.polynomialTangent_units line 45
  9. def OAI.GrahamSpherical.fractionTangent line 50
  10. theorem OAI.GrahamSpherical.fractionTangent_fst line 54
  11. def OAI.GrahamSpherical.fractionDerivation line 66
  12. theorem OAI.GrahamSpherical.fractionDerivation_X line 82
  13. theorem OAI.GrahamSpherical.exists_derivation_adjoin_coordinate line 92

    Source documentation

    A selected algebraically independent coordinate admits a unit-valued derivation on the field generated by all coordinates.

    theorem exists_derivation_adjoin_coordinate {ι : Type*} (b : ι → ℝ)
    (hb : AlgebraicIndependent ℚ b) (i : ι) :
    ∃ D : Derivation ℤ (IntermediateField.adjoin ℚ (Set.range b))
      (IntermediateField.adjoin ℚ (Set.range b)),
      D ⟨b i, IntermediateField.subset_adjoin ℚ (Set.range b) ⟨i, rfl⟩⟩ = 1 := by
…