NYLL
Module

Place_evalAt_mul.lean

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

Module documentation

Place evalAt mul

Evaluation at a rational place preserves the product of two integral functions.

Imports1
Imported by14

Declarations

theorem

evalAt_mul

L27 ↗
AlgebraicCurve.Place.evalAt_mul
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_mul
open IsLocalRing AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_mul {K F : Type*} [Field K] [Field F] [Algebra K F]
  (v : Place K F) (hv : v.IsRational) {f g : F} (hf : f ∈ v.toValuationSubring) (hg :
  g ∈ v.toValuationSubring) : v.evalAt (f * g) = v.evalAt f * v.evalAt g

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