Module

SemilinearAut_ramificationIndex_smul.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ramificationIndex_smul

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut ramification Index smul

Imports2

Imported by3

theorem

solution

L30 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_ramificationIndex_smul.solution

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_ramificationIndex_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') : (g' • w).ramificationIndex F = w.ramificationIndex F

theorem

ramificationIndex_smul

L52 ↗

AlgebraicCurve.SemilinearAut.ramificationIndex_smul

Source context 1 command