Module

Finite_setOf_ord_ne_zero_of_finiteDimensional.lean

Nyll.AlgebraicCurves.Places.Finite_setOf_ord_ne_zero_of_finiteDimensional

3 declarations indexed from sourceView source ↗

Module documentation

Finite setOf ord ne zero of finiteDimensional

A function in a finite extension of a rational function field has nonzero order at only finitely many places.

Imports7

Nyll.AlgebraicCurves.Places.OverDVR
Nyll.AlgebraicCurves.Places.Place_ord_nonneg_of_mem
Nyll.AlgebraicCurves.Places.Place_mem_of_ord_nonneg
Nyll.AlgebraicCurves.Places.Place_exists_ord_pos
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_finite_setOf_ord_ne_zero
Mathlib.FieldTheory.Minpoly.Field
Mathlib.FieldTheory.RatFunc.Basic

Imported by2

theorem

aeval_mem

L54 ↗

AlgebraicCurve.Place.aeval_mem

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finite_setOf_ord_ne_zero_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding exists_ord_pos
section SupportTransfer
open Polynomial
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
  [FiniteDimensional F F']
variable (w : Place K F')
omit [FiniteDimensional F F'] in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.aeval_mem {Q : Polynomial F} {x : F'}
    (hcoeff : ∀ i, algebraMap F F' (Q.coeff i) ∈ w.toValuationSubring)
    (hx : x ∈ w.toValuationSubring) :
    Polynomial.aeval x Q ∈ w.toValuationSubring

theorem

exists_coeff_ord_ne_zero

L63 ↗

AlgebraicCurve.Place.exists_coeff_ord_ne_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finite_setOf_ord_ne_zero_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding exists_ord_pos
section SupportTransfer
open Polynomial
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
  [FiniteDimensional F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_coeff_ord_ne_zero {f : F'} (hf : f ≠ 0)
  (hford : w.ord f ≠ 0) :
    ∃ i < (minpoly F f).natDegree, (minpoly F f).coeff i ≠ 0 ∧
      w.ord (algebraMap F F' ((minpoly F f).coeff i)) ≠ 0

theorem

finite_setOf_ord_ne_zero_of_finiteDimensional

L117 ↗

AlgebraicCurve.finite_setOf_ord_ne_zero_of_finiteDimensional

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Finite_setOf_ord_ne_zero_of_finiteDimensional
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.finite_setOf_ord_ne_zero_of_finiteDimensional {K F' : Type*}
  [Field K] [Field F'] [Algebra K F']
    [Algebra (RatFunc K) F'] [IsScalarTower K (RatFunc K) F'] [FiniteDimensional (RatFunc K) F']
      [Algebra.IsSeparable (RatFunc K) F']
    {f : F'} (hf : f ≠ 0) : {w : Place K F' | w.ord f ≠ 0}.Finite

Module documentation

Finite setOf ord ne zero of finiteDimensional

Declarations

aeval_mem

exists_coeff_ord_ne_zero

finite_setOf_ord_ne_zero_of_finiteDimensional