AlgebraicExtension.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GrahamSpherical.AlgebraicExtension.value line 18
Source documentation
The value forced by the native derivation on a finite simple subextension.
```
noncomputable def value (x : K) : K :=
…
```
theorem OAI.GrahamSpherical.AlgebraicExtension.value_eq line 22
Source documentation
All finite subextensions compute the same derivative of a given element.
```
theorem value_eq (L : IntermediateField F K) [FiniteDimensional F L]
    (x : K) (hx : x ∈ L) :
    value (F := F) x = ((Differential.deriv (⟨x, hx⟩ : L) : L) : K) := by
…
```
Mentions: OAI.GrahamSpherical.AlgebraicExtension.value
theorem OAI.GrahamSpherical.AlgebraicExtension.value_zero line 30
theorem OAI.GrahamSpherical.AlgebraicExtension.value_add line 35
theorem OAI.GrahamSpherical.AlgebraicExtension.value_mul line 44
def OAI.GrahamSpherical.AlgebraicExtension.differentialAlgebraic line 60
Source documentation
Extension to an arbitrary algebraic field extension in characteristic zero.
```
noncomputable def differentialAlgebraic : Differential K where
…
```
theorem OAI.GrahamSpherical.AlgebraicExtension.value_algebraMap line 66
theorem OAI.GrahamSpherical.AlgebraicExtension.differentialAlgebraAlgebraic line 74
theorem OAI.GrahamSpherical.AlgebraicExtension.exists_extension line 82
Source documentation
Explicit derivation interface, avoiding any preexisting derivative on the target.
```
theorem exists_extension (D : Derivation ℤ F F) :
    ∃ E : Derivation ℤ K K,
      ∀ x : F, E (algebraMap F K x) = algebraMap F K (D x) := by
…
```