Module

IsIntegral_adjoin_of_forall_ord_nonneg.lean

Nyll.AlgebraicCurves.Places.IsIntegral_adjoin_of_forall_ord_nonneg

3 declarations indexed from sourceView source ↗

Module documentation

Is Integral adjoin of forall ord nonneg

Imports4

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

isIntegral_of_mem_adjoin_inv

L30 ↗

AlgebraicCurves.Places.Proofs.IsIntegral_adjoin_of_forall_ord_nonneg.INTGlue.isIntegral_of_mem_adjoin_inv

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.IsIntegral_adjoin_of_forall_ord_nonneg
open AlgebraicCurve Polynomial
namespace INTGlue

Lean source · statement

theorem isIntegral_of_mem_adjoin_inv {A F : Type*} [CommRing A] [Field F] [Algebra A F]
    {z : F} (hz0 : z ≠ 0) (hmem : z ∈ Algebra.adjoin A ({z⁻¹} : Set F)) : IsIntegral A z

theorem

isIntegral_of_forall_valuationSubring

L62 ↗

AlgebraicCurves.Places.Proofs.IsIntegral_adjoin_of_forall_ord_nonneg.INTGlue.isIntegral_of_forall_valuationSubring

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.IsIntegral_adjoin_of_forall_ord_nonneg
open AlgebraicCurve Polynomial
namespace INTGlue

Lean source · statement

theorem isIntegral_of_forall_valuationSubring {F : Type*} [Field F] (A : Subring F) (z : F)
    (h : ∀ V : ValuationSubring F, A ≤ V.toSubring → z ∈ V) : IsIntegral A z

theorem

isIntegral_adjoin_of_forall_ord_nonneg

L117 ↗

AlgebraicCurve.isIntegral_adjoin_of_forall_ord_nonneg

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.IsIntegral_adjoin_of_forall_ord_nonneg
open AlgebraicCurve Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.isIntegral_adjoin_of_forall_ord_nonneg {K F : Type*} [Field K] [Field
  F] [Algebra K F] [CharZero K] (t : F)
    (_ht : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set F)) F]
    [AlgebraicCurve.HasPrincipalDivisors K F] (z : F)
    (hz : ∀ v : AlgebraicCurve.Place K F, 0 ≤ v.ord t → 0 ≤ v.ord z) :
    IsIntegral (Algebra.adjoin K ({t} : Set F)) z

Module documentation

Is Integral adjoin of forall ord nonneg

Declarations

isIntegral_of_mem_adjoin_inv

isIntegral_of_forall_valuationSubring

isIntegral_adjoin_of_forall_ord_nonneg