Module

Place_evalAt_congr.lean

Nyll.AlgebraicCurves.Places.Place_evalAt_congr

1 declaration indexed from sourceView source ↗

Module documentation

Place evalAt congr

Evaluation at a place is unchanged when two integral functions have the same residue.

Imports2

Imported by9

theorem

evalAt_congr

L36 ↗

AlgebraicCurve.Place.evalAt_congr

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_congr
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 IsDedekindDomain WithZero IsLocalRing AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.evalAt_congr {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) {f g : F} (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) (h :
  f - g = 0 ∨ 0 < v.ord (f - g)) : v.evalAt f = v.evalAt g

Module documentation

Place evalAt congr

Declarations

evalAt_congr