AlgebraicCurve.Place.evalAt_map_eq_of_comap_eq
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_map_eq_of_comap_eq
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_map_eq_of_comap_eq {K F K' F' : Type*}
[Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
(τ : K →+* K') (φ : F →+* F') (hφ : ∀ c : K, φ (algebraMap K F c) = algebraMap K' F' (τ c))
(v : Place K F) (v' : Place K' F') (h : v'.toValuationSubring.comap φ = v.toValuationSubring)
(hv : v.IsRational) {x : F} (hx : x ∈ v.toValuationSubring) :
v'.evalAt (φ x) = τ (v.evalAt x)