NYLL
Module

ConstantsAreBase_of_deg_eq_one.lean

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

Module documentation

ConstantsAreBase of deg eq one

A place of degree one identifies the constant field with the base field.

Imports4
Imported by11

Declarations

theorem

constantsAreBase_of_deg_eq_one

L30 ↗
AlgebraicCurve.constantsAreBase_of_deg_eq_one
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_deg_eq_one
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.constantsAreBase_of_deg_eq_one {K F : Type*} [Field K] [Field F]
  [Algebra K F]
    [AlgebraicCurve.HasPrincipalDivisors K F]
    (v₀ : AlgebraicCurve.Place K F) (hdeg : v₀.deg = 1) :
    AlgebraicCurve.ConstantsAreBase K F

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