Module

Place_mem_toValuationSubring_of_isIntegral_adjoin.lean

Nyll.AlgebraicCurves.Places.Place_mem_toValuationSubring_of_isIntegral_adjoin

5 declarations indexed from sourceView source ↗

Module documentation

Place mem to Valuation Subring of is Integral adjoin

Imports2

Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.RingTheory.Valuation.Integral

Imported by5

def

placeSubalgebra

L30 ↗

AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin.ModularCurve.QexpN.placeSubalgebra

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin
open AlgebraicCurve
namespace ModularCurve
namespace QexpN

Lean source · statement

def placeSubalgebra {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) :
    Subalgebra K F

theorem

mem_placeSubalgebra

L34 ↗

AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin.ModularCurve.QexpN.mem_placeSubalgebra

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin
open AlgebraicCurve
namespace ModularCurve
namespace QexpN

Lean source · statement

theorem mem_placeSubalgebra {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {y : F} :
    y ∈ placeSubalgebra v ↔ y ∈ v.toValuationSubring

theorem

valuationSubring_integers

L38 ↗

AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin.ModularCurve.QexpN.valuationSubring_integers

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin
open AlgebraicCurve
namespace ModularCurve
namespace QexpN

Lean source · statement

theorem valuationSubring_integers {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) :
    (v.toValuationSubring.valuation).Integers v.toValuationSubring

theorem

mem_of_isIntegral_adjoin

L46 ↗

AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin.ModularCurve.QexpN.mem_of_isIntegral_adjoin

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin
open AlgebraicCurve
namespace ModularCurve
namespace QexpN

Lean source · statement

theorem mem_of_isIntegral_adjoin {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {j x : F} (hj : j ∈ v.toValuationSubring)
    (hx : IsIntegral (Algebra.adjoin K {j}) x) : x ∈ v.toValuationSubring

theorem

mem_toValuationSubring_of_isIntegral_adjoin

L66 ↗

AlgebraicCurve.Place.mem_toValuationSubring_of_isIntegral_adjoin

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_toValuationSubring_of_isIntegral_adjoin
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_toValuationSubring_of_isIntegral_adjoin {K F : Type*}
  [Field K] [Field F] [Algebra K F] (v : Place K F) {j x : F} (hj : j ∈ v.toValuationSubring) (hx
  : IsIntegral (Algebra.adjoin K {j}) x) : x ∈ v.toValuationSubring

Module documentation

Place mem to Valuation Subring of is Integral adjoin

Declarations

placeSubalgebra

mem_placeSubalgebra

valuationSubring_integers

mem_of_isIntegral_adjoin

mem_toValuationSubring_of_isIntegral_adjoin