NYLL
Module

RationalFunctionField_deg_placeInfty.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_placeInfty
1 declaration indexed from sourceView source ↗

Module documentation

RationalFunctionField deg placeInfty

The place at infinity of a rational function field has degree one.

Imports8
Imported by26

Declarations

theorem

deg_placeInfty

L39 ↗
AlgebraicCurve.RationalFunctionField.deg_placeInfty
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_deg_placeInfty
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open IsDedekindDomain AlgebraicCurve AlgebraicCurve.RationalFunctionField
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.deg_placeInfty (K : Type*) [Field K]
  [DecidableEq (RatFunc K)] : (placeInfty K).deg = 1

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