AlgebraicCurve.Place.restrictAlong_eq_smul_of_forall_eq_inv_smul_pow
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_eq_smul_of_forall_eq_inv_smul_pow
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.restrictAlong_eq_smul_of_forall_eq_inv_smul_pow
{K : Type*} [Field K] {L : Type*} [Field L] [Algebra K L]
(p : ℕ) (hp : p ≠ 0) (g : SemilinearAut K L)
(Φ : L →ₐ[K] L) (hΦi : Φ.toRingHom.IsIntegral) (hΦ : ∀ f : L, Φ f = (g⁻¹ • f) ^ p)
(w : AlgebraicCurve.Place K L) :
w.restrictAlong Φ hΦi = g • w