Module

ValuationSubring_isPrincipalIdealRing_of_finiteDimensional_adjoin.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_isPrincipalIdealRing_of_finiteDimensional_adjoin

4 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring is Principal Ideal Ring of finite Dimensional adjoin

Imports10

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.Minpoly.Finite
Mathlib.RingTheory.Valuation.Discrete.Basic
Mathlib.RingTheory.Valuation.Integral
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Mathlib.Data.Nat.Factorial.Basic
Mathlib.Tactic.Push
Mathlib.Tactic.NormNum

Imported by6

theorem

valuationSubring_eq_top_of_isAlgebraic

L38 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal.P2mFunctionFieldPlacesDiscrete.valuationSubring_eq_top_of_isAlgebraic

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal
open Polynomial
namespace P2mFunctionFieldPlacesDiscrete
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem valuationSubring_eq_top_of_isAlgebraic (E : Type*) [Field E] [Algebra E F]
    [Algebra.IsAlgebraic E F] (O : ValuationSubring F)
    (hE : ∀ a : E, algebraMap E F a ∈ O) : O = ⊤

theorem

core

L50 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal.P2mFunctionFieldPlacesDiscrete.core

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal
open Polynomial
namespace P2mFunctionFieldPlacesDiscrete
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem core (y : F) [FiniteDimensional (IntermediateField.adjoin K ({y} : Set F)) F]
    (O : ValuationSubring F) (hK : ∀ a : K, algebraMap K F a ∈ O) (hO : O ≠ ⊤)
    (hy : y ∈ O) (hyt : Transcendental K y) : IsPrincipalIdealRing O

theorem

isPrincipalIdealRing_of_finiteDimensional_adjoin

L236 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal.P2mFunctionFieldPlacesDiscrete.isPrincipalIdealRing_of_finiteDimensional_adjoin

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal
open Polynomial
namespace P2mFunctionFieldPlacesDiscrete
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem isPrincipalIdealRing_of_finiteDimensional_adjoin {K F : Type*} [Field K] [Field F]
  [Algebra K F] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (O : ValuationSubring F) (hK : ∀ a : K, algebraMap K F a ∈ O) (hO : O ≠ ⊤) :
    IsPrincipalIdealRing O

theorem

isPrincipalIdealRing_of_finiteDimensional_adjoin

L273 ↗

ValuationSubring.isPrincipalIdealRing_of_finiteDimensional_adjoin

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubringPrincipalIdeal
open Polynomial

Lean source · statement

theorem _root_.ValuationSubring.isPrincipalIdealRing_of_finiteDimensional_adjoin
    {K F : Type*} [Field K] [Field F] [Algebra K F] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (O : ValuationSubring F) (hK : ∀ a : K, algebraMap K F a ∈ O) (hO : O ≠ ⊤) :
    IsPrincipalIdealRing O

Module documentation

Valuation Subring is Principal Ideal Ring of finite Dimensional adjoin

Declarations

valuationSubring_eq_top_of_isAlgebraic

core

isPrincipalIdealRing_of_finiteDimensional_adjoin

isPrincipalIdealRing_of_finiteDimensional_adjoin