theorem
L25 ↗hasValue_smul_iff
AlgebraicCurve.Place.hasValue_smul_iff
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_smul_iff
open AlgebraicCurve IsLocalRingLean source · statement
theorem _root_.AlgebraicCurve.Place.hasValue_smul_iff {K F : Type*} [Field K] [Field F] [Algebra K
F]
(σ : F ≃ₐ[K] F) (v : Place K F) (g : F) (a : K) :
(σ • v).HasValue (σ g) a ↔ v.HasValue g a