NYLL
Module

Place_evalAt_zpow.lean

Nyll.AlgebraicCurves.Places.Place_evalAt_zpow
1 declaration indexed from sourceView source ↗

Module documentation

Place evalAt zpow

Evaluation at a rational place preserves integer powers of a nonzero function of order zero.

Imports4
Imported by9

Declarations

theorem

evalAt_zpow

L31 ↗
AlgebraicCurve.Place.evalAt_zpow
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_zpow
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_zpow {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) (hv : v.IsRational) {f : F} (hf : f ≠ 0) (h : v.ord f = 0) (n : ℤ) : v.evalAt
  (f ^ n) = v.evalAt f ^ n

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