NYLL
Module

Infinity.lean

Nyll.AlgebraicCurves.Places.Rational.Infinity
3 declarations indexed from sourceView source ↗

Module documentation

Infinity

The valuation at infinity defines a place of a rational function field.

Imports3
Imported by53

Declarations

theorem

nontrivial_valueGroup_inftyValuation

L33 ↗
AlgebraicCurve.RationalFunctionField.nontrivial_valueGroup_inftyValuation
Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
Lean source · statement
theorem nontrivial_valueGroup_inftyValuation :
    Nontrivial (MonoidWithZeroHom.valueGroup (.ofClass (RatFunc.inftyValuation K)))
def

placeInfty

L43 ↗
AlgebraicCurve.RationalFunctionField.placeInfty
Documentation

The place defined by the rational-function-field valuation at infinity.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
Lean source · statement
def placeInfty : Place K (RatFunc K)
theorem

placeInfty_toValuationSubring

L56 ↗
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
Lean source · statement
theorem placeInfty_toValuationSubring :
    (placeInfty K).toValuationSubring = (RatFunc.inftyValuation K).valuationSubring

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