NYLL
Module

Finite_intermediateField_of_transcendental_mem.lean

Nyll.AlgebraicCurves.FunctionFields.Finite_intermediateField_of_transcendental_mem
2 declarations indexed from sourceView source ↗

Module documentation

Finite intermediate Field of transcendental mem

Imports2
  • Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
  • Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Imported by1

Declarations

theorem

finiteDimensional_adjoin_of_transcendental

L30 ↗
AlgebraicCurves.FunctionFields.Proofs.Finite_intermediateField_of_transcendental_mem.S2Finite.finiteDimensional_adjoin_of_transcendental
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_intermediateField_of_transcendental_mem
namespace S2Finite
open IntermediateField
variable {K F : Type} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteDimensional_adjoin_of_transcendental {x₀ : F} (hx₀ : Transcendental K x₀)
    (hfd : FiniteDimensional K⟮x₀⟯ F) {t : F} (ht : Transcendental K t) : FiniteDimensional K⟮t⟯ F
theorem

finite_intermediateField_of_transcendental_mem

L69 ↗
AlgebraicCurve.finite_intermediateField_of_transcendental_mem
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finite_intermediateField_of_transcendental_mem
open IntermediateField in
Lean source · statement
theorem _root_.AlgebraicCurve.finite_intermediateField_of_transcendental_mem
    (K L : Type) [Field K] [Field L] [Algebra K L]
    (E : IntermediateField K L) (t : L) (htE : t ∈ E) (ht : Transcendental K t)
    (hfg : ∃ x : L, Transcendental K x ∧ FiniteDimensional ↥(IntermediateField.adjoin K ({x} : Set
      L)) L) :
    Module.Finite ↥E L

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.