Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_ne_zero

theorem

deg_ne_zero

AlgebraicCurve.RationalFunctionField.deg_ne_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_deg_ne_zero
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve IsDedekindDomain Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.deg_ne_zero {K : Type*} [Field K] (v : Place K
  (RatFunc K)) : v.deg ≠ 0

RationalFunctionField_deg_ne_zero.lean

Module documentation

Rational Function Field deg ne zero

deg_ne_zero

Module documentation

Rational Function Field deg ne zero

Declarations

deg_ne_zero