Module

Place_ord_eq_neg_log_of_valuationSubring_eq.lean

Nyll.AlgebraicCurves.Places.Place_ord_eq_neg_log_of_valuationSubring_eq

2 declarations indexed from sourceView source ↗

Module documentation

Place ord eq neg log of valuationSubring eq

An identification of valuation subrings expresses the order of a place as the negative logarithm of the corresponding discrete valuation.

Imports2

Imported by12

theorem

le_exp_neg_one_of_lt_one

L44 ↗

AlgebraicCurves.Places.Proofs.Place_ord_eq_neg_log_of_valuationSubring_eq.AlgebraicCurve.WFa.le_exp_neg_one_of_lt_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_eq_neg_log_of_valuationSubring_eq
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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WFa
open _root_.AlgebraicCurve

Lean source · statement

theorem le_exp_neg_one_of_lt_one {x : ℤᵐ⁰} (hx : x < 1) : x ≤ exp (-1 : ℤ)

theorem

ord_eq_neg_log_of_valuationSubring_eq

L55 ↗

AlgebraicCurve.Place.ord_eq_neg_log_of_valuationSubring_eq

Source context 8 commands