AlgebraicCurve.Place.evalAt_smul_smul_eq_baseAut_evalAt
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_smul_smul_eq_baseAut_evalAt
open AlgebraicCurve IsLocalRingLean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_smul_smul_eq_baseAut_evalAt
{K F : Type*} [Field K] [Field F] [Algebra K F]
(σ : SemilinearAut K F) (v : AlgebraicCurve.Place K F)
(hv : v.IsRational) (hσv : (σ • v).IsRational) (f : F) :
(σ • v).evalAt (σ • f) = SemilinearAut.baseAut σ (v.evalAt f)