RealDerivation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GrahamSpherical.exists_real_derivation line 12
Source documentation
Prescribe a derivation at any transcendental real, with an arbitrary real value. The final scalar need not belong to the rational-function subfield.
```
theorem exists_real_derivation (a c : ℝ) (ha : Transcendental ℚ a) :
    ∃ D : Derivation ℤ ℝ ℝ, D a = c := by
…
```