Module

Place_transcendental_of_ord_ne_zero.lean

Nyll.AlgebraicCurves.Places.Place_transcendental_of_ord_ne_zero

3 declarations indexed from sourceView source ↗

Module documentation

Place transcendental of ord ne zero

Imports4

Nyll.AlgebraicCurves.Places.OverDVR
Mathlib.RingTheory.Algebraic.Basic
Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.RingTheory.Algebraic.Defs

Imported by19

theorem

mem_of_isAlgebraic

L39 ↗

AlgebraicCurves.Places.Proofs.Place_transcendental_of_ord_ne_zero.AlgebraicCurve.Place.FF2R0.mem_of_isAlgebraic

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_transcendental_of_ord_ne_zero
noncomputable section
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FF2R0
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)

Lean source · statement

theorem mem_of_isAlgebraic {x : F} (hx : IsAlgebraic K x) : x ∈ v.toValuationSubring

theorem

ord_eq_zero_of_isAlgebraic'

L47 ↗

AlgebraicCurves.Places.Proofs.Place_transcendental_of_ord_ne_zero.AlgebraicCurve.Place.FF2R0.ord_eq_zero_of_isAlgebraic'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_transcendental_of_ord_ne_zero
noncomputable section
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FF2R0
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)

Lean source · statement

theorem ord_eq_zero_of_isAlgebraic' {x : F} (hx : IsAlgebraic K x) : v.ord x = 0

theorem

transcendental_of_ord_ne_zero

L59 ↗

AlgebraicCurve.Place.transcendental_of_ord_ne_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_transcendental_of_ord_ne_zero
noncomputable section
open Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.Place.transcendental_of_ord_ne_zero {K F : Type*} [Field K] [Field
  F] [Algebra K F] (v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t ≠ 0) :
    Transcendental K t

Module documentation

Place transcendental of ord ne zero

Declarations

mem_of_isAlgebraic

ord_eq_zero_of_isAlgebraic'

transcendental_of_ord_ne_zero