AlgebraicCurve.Place.HasValue.smul
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing
namespace AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]Lean source · statement
theorem HasValue.smul {v : Place K F} {f : F} {a : K} (g : SemilinearAut K F)
(h : v.HasValue f a) : (g • v).HasValue (g • f) (SemilinearAut.baseAut g a)