Module

SemilinearAut_ord_algebraMap_smul.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ord_algebraMap_smul

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut ord algebra Map smul

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by2

theorem

solution

L28 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_ord_algebraMap_smul.solution

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_ord_algebraMap_smul
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable section

Lean source · statement

theorem solution {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] {g : SemilinearAut K F} {g' : SemilinearAut K F'} (hgg' : IntertwinesAlong
  (algebraMap F F') g g') (w : Place K F') (f : F) : (g' • w).ord (algebraMap F F' f) = w.ord
  (algebraMap F F' (g⁻¹ • f))

theorem

ord_algebraMap_smul

L44 ↗

AlgebraicCurve.SemilinearAut.ord_algebraMap_smul

Source context 1 command