AlgebraicCurve.Place.restrictAlong_algEquiv_eq_ofAlgAut_symm_smul
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_algEquiv_eq_ofAlgAut_symm_smul
open AlgebraicCurve
open scoped PointwiseLean source · statement
theorem _root_.AlgebraicCurve.Place.restrictAlong_algEquiv_eq_ofAlgAut_symm_smul
{K F : Type*} [Field K] [Field F] [Algebra K F]
(σ : F ≃ₐ[K] F) (hσ : σ.toAlgHom.toRingHom.IsIntegral) (v : Place K F) :
v.restrictAlong σ.toAlgHom hσ = SemilinearAut.ofAlgAut σ.symm • v