NYLL
Module

Place_ord_algebraMap.lean

Nyll.AlgebraicCurves.Places.Place_ord_algebraMap
4 declarations indexed from sourceView source ↗

Module documentation

Place ord algebraMap

Orders of nonzero constants vanish at places trivial on the base field.

Imports1
Imported by26

Declarations

theorem

isUnit_algebraMap

L40 ↗
AlgebraicCurve.Place.isUnit_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_algebraMap
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isUnit_algebraMap {c : K} (hc : c ≠ 0) :
    IsUnit (algebraMap K v.toValuationSubring c)
theorem

adicValuation_algebraMap

L45 ↗
AlgebraicCurve.Place.adicValuation_algebraMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_algebraMap
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.adicValuation_algebraMap {c : K} (hc : c ≠ 0) :
    v.adicValuation (algebraMap K F c) = 1
theorem

rowMain

L51 ↗
AlgebraicCurves.Places.Proofs.Place_ord_algebraMap.AlgebraicCurve.Place.rowMain
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_algebraMap
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem rowMain (c : K) : v.ord (algebraMap K F c) = 0
theorem

ord_algebraMap

L64 ↗
AlgebraicCurve.Place.ord_algebraMap
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_algebraMap
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_ord_algebraMap.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_algebraMap {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) (c : K) :
    v.ord (algebraMap K F c) = 0

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.