NYLL
Module

FiniteDimensional_adjoin_of_transcendental.lean

Nyll.AlgebraicCurves.FunctionFields.FiniteDimensional_adjoin_of_transcendental
3 declarations indexed from sourceView source ↗

Module documentation

Finite Dimensional adjoin of transcendental

Imports8
  • Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  • Mathlib.RingTheory.AlgebraicIndependent.Transcendental
  • Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  • Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
  • Mathlib.RingTheory.Algebraic.Defs
  • Mathlib.LinearAlgebra.FiniteDimensional.Defs
Imported by15

Declarations

theorem

isAlgebraic_adjoin_of_transcendental'

L37 ↗
AlgebraicCurves.FunctionFields.Proofs.FiniteDimensional_adjoin_of_transcendental.AlgebraicCurve.FF2KE3.isAlgebraic_adjoin_of_transcendental'
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FiniteDimensional_adjoin_of_transcendental
open Set Cardinal
namespace AlgebraicCurve
namespace FF2KE3
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isAlgebraic_adjoin_of_transcendental' (x : F)
    [halg : Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    {t : F} (ht : Transcendental K t) :
    Algebra.IsAlgebraic (IntermediateField.adjoin K ({t} : Set F)) F
theorem

finiteDimensional_adjoin_of_transcendental'

L66 ↗
AlgebraicCurves.FunctionFields.Proofs.FiniteDimensional_adjoin_of_transcendental.AlgebraicCurve.FF2KE3.finiteDimensional_adjoin_of_transcendental'
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FiniteDimensional_adjoin_of_transcendental
open Set Cardinal
namespace AlgebraicCurve
namespace FF2KE3
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteDimensional_adjoin_of_transcendental' (x : F)
    [hfin : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {t : F} (ht : Transcendental K t) :
    FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F
theorem

finiteDimensional_adjoin_of_transcendental

L100 ↗
AlgebraicCurve.finiteDimensional_adjoin_of_transcendental
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FiniteDimensional_adjoin_of_transcendental
open Set Cardinal
Lean source · statement
theorem _root_.AlgebraicCurve.finiteDimensional_adjoin_of_transcendental {K F : Type*} [Field K]
  [Field F] [Algebra K F] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] {t : F} (ht : Transcendental
      K t) :
    FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F

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