NYLL
Module

Place_exists_ord_pos.lean

Nyll.AlgebraicCurves.Places.Place_exists_ord_pos
2 declarations indexed from sourceView source ↗

Module documentation

Place exists ord pos

The maximal ideal of a place supplies a nonzero element of positive order.

Imports1
Imported by6

Declarations

theorem

rowMain

L40 ↗
AlgebraicCurves.Places.Place_exists_ord_pos.AlgebraicCurve.Place.rowMain
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_exists_ord_pos
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 rowMain : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f
theorem

exists_ord_pos

L54 ↗
AlgebraicCurve.Place.exists_ord_pos
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_exists_ord_pos
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve _root_.AlgebraicCurves.Places.Place_exists_ord_pos.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_pos {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) :
    ∃ f : F, f ≠ 0 ∧ 0 < v.ord f

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