NYLL
Module

IsCurveOver_trdeg_eq_one.lean

Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_trdeg_eq_one
1 declaration indexed from sourceView source ↗

Module documentation

Is Curve Over trdeg eq one

Imports3
Imported by1

Declarations

theorem

trdeg_eq_one

L28 ↗
AlgebraicCurve.IsCurveOver.trdeg_eq_one
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOver_trdeg_eq_one
open AlgebraicCurve IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
theorem _root_.AlgebraicCurve.IsCurveOver.trdeg_eq_one
    (K F : Type*) [Field K] [Field F] [Algebra K F] [PerfectField K]
    [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    Algebra.trdeg K F = 1

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