Module

Place_finite_setOf_deg_eq.lean

Nyll.AlgebraicCurves.Places.Place_finite_setOf_deg_eq

5 declarations indexed from sourceView source ↗

Module documentation

Place finite set Of deg eq

Imports6

Imported by3

theorem

finite_setOf_natDegree_le

L43 ↗

AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq.AlgebraicCurve.Place.FiniteSetOfDegEqAux.finite_setOf_natDegree_le

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
open _root_.IntermediateField
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteSetOfDegEqAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem finite_setOf_natDegree_le (K : Type*) [Field K] [Finite K] (d : ℕ) :
    {g : K[X] | g.natDegree ≤ d}.Finite

theorem

finite_heightOneSpectrum_of_deg_eq

L53 ↗

AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq.AlgebraicCurve.Place.FiniteSetOfDegEqAux.finite_heightOneSpectrum_of_deg_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
open _root_.IntermediateField
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteSetOfDegEqAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem finite_heightOneSpectrum_of_deg_eq (K : Type*) [Field K] [Finite K] (d : ℕ) :
    {w : HeightOneSpectrum K[X] |
      (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).deg = d}.Finite

theorem

finite_setOf_ratFunc_place_deg_eq

L66 ↗

AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq.AlgebraicCurve.Place.FiniteSetOfDegEqAux.finite_setOf_ratFunc_place_deg_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
open _root_.IntermediateField
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteSetOfDegEqAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem finite_setOf_ratFunc_place_deg_eq (K : Type*) [Field K] [Finite K] (d : ℕ) :
    {v : Place K (RatFunc K) | v.deg = d}.Finite

theorem

exists_ratFunc_intermediate

L82 ↗

AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq.AlgebraicCurve.Place.FiniteSetOfDegEqAux.exists_ratFunc_intermediate

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
open _root_.IntermediateField
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteSetOfDegEqAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem exists_ratFunc_intermediate (K F : Type*) [Field K] [Finite K] [Field F] [Algebra K F]
    [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    ∃ (_ : Algebra (RatFunc K) F) (_ : IsScalarTower K (RatFunc K) F)
      (_ : Algebra.IsIntegral (RatFunc K) F), Module.Finite (RatFunc K) F

theorem

finite_setOf_deg_eq

L109 ↗

AlgebraicCurve.Place.finite_setOf_deg_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_finite_setOf_deg_eq
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open _root_.Polynomial
open _root_.IntermediateField
open scoped Polynomial
open AlgebraicCurve.Place.FiniteSetOfDegEqAux in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.finite_setOf_deg_eq
    (K F : Type*) [Field K] [Finite K] [Field F] [Algebra K F]
    [Algebra.EssFiniteType K F] [IsCurveOver K F] (d : ℕ) :
    {v : Place K F | v.deg = d}.Finite

Module documentation

Place finite set Of deg eq

Declarations

finite_setOf_natDegree_le

finite_heightOneSpectrum_of_deg_eq

finite_setOf_ratFunc_place_deg_eq

exists_ratFunc_intermediate

finite_setOf_deg_eq