Module

Exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one.lean

Nyll.AlgebraicCurves.Differentials.Exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one

1 declaration indexed from sourceView source ↗

Module documentation

Find a separable transcendental coordinate when the differential module has rank one.

Imports2

Mathlib.RingTheory.Unramified.Field
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Imported by6

theorem

exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one

L29 ↗

AlgebraicCurve.exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace Exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one
universe u v
open IntermediateField

Lean source · statement

theorem
    _root_.AlgebraicCurve.exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [Algebra.EssFiniteType K F]
    [Algebra.Transcendental K F] (hΩ : Module.finrank F Ω[F⁄K] = 1) :
    ∃ t : F, Transcendental K t ∧ FiniteDimensional K⟮t⟯ F ∧ Algebra.IsSeparable K⟮t⟯ F

Module documentation

Declarations

exists_transcendental_isSeparable_of_finrank_kaehlerDifferential_eq_one