Module

Place_restrict_ofAlgAut_smul.lean

Nyll.AlgebraicCurves.Places.Place_restrict_ofAlgAut_smul

1 declaration indexed from sourceView source ↗

Module documentation

Place restrict of Alg Aut smul

Imports2

Imported by8

theorem

restrict_ofAlgAut_smul

L45 ↗

AlgebraicCurve.Place.restrict_ofAlgAut_smul

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrict_ofAlgAut_smul
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped Pointwise
open _root_.AlgebraicCurve.Place
  _root_.AlgebraicCurves.Places.Proofs.Place_restrict_ofAlgAut_smul.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.restrict_ofAlgAut_smul {K F' M : Type*} [Field K] [Field F']
  [Field M]
    [Algebra K F'] [Algebra K M] [Algebra F' M] [IsScalarTower K F' M]
    [Algebra.IsIntegral F' M] (σ : M ≃ₐ[F'] M) (W : Place K M) :
    (SemilinearAut.ofAlgAut (σ.restrictScalars K) • W).restrict F' = W.restrict F'

Module documentation

Place restrict of Alg Aut smul

Declarations

restrict_ofAlgAut_smul