Module

IsAlgebraic_adjoin_of_transcendental.lean

Nyll.AlgebraicCurves.FunctionFields.IsAlgebraic_adjoin_of_transcendental

2 declarations indexed from sourceView source ↗

Module documentation

Is Algebraic adjoin of transcendental

Imports7

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

Imported by8

theorem

isAlgebraic_adjoin_of_transcendental'

L36 ↗

AlgebraicCurves.FunctionFields.Proofs.IsAlgebraic_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.IsAlgebraic_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

isAlgebraic_adjoin_of_transcendental

L67 ↗

AlgebraicCurve.isAlgebraic_adjoin_of_transcendental

Source context 3 commands