Module

EssFiniteType_of_transcendental_of_finiteDimensional.lean

Nyll.AlgebraicCurves.FunctionFields.EssFiniteType_of_transcendental_of_finiteDimensional

1 declaration indexed from sourceView source ↗

Module documentation

Ess Finite Type of transcendental of finite Dimensional

Imports2

Mathlib.FieldTheory.RatFunc.AsPolynomial
Mathlib.RingTheory.EssentialFiniteness

Imported by33

theorem

essFiniteType_of_transcendental_of_finiteDimensional

L27 ↗

AlgebraicCurve.essFiniteType_of_transcendental_of_finiteDimensional

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.EssFiniteType_of_transcendental_of_finiteDimensional
open IntermediateField Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.essFiniteType_of_transcendental_of_finiteDimensional
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    {x : F} (htr : Transcendental K x)
    (hfd : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    Algebra.EssFiniteType K F

Module documentation

Ess Finite Type of transcendental of finite Dimensional

Declarations

essFiniteType_of_transcendental_of_finiteDimensional