Module

Place_card_fiberOver_mul_ramificationIndex_mul_inertiaDeg.lean

Nyll.AlgebraicCurves.Places.Place_card_fiberOver_mul_ramificationIndex_mul_inertiaDeg

1 declaration indexed from sourceView source ↗

Module documentation

Place card fiber Over mul ramification Index mul inertia Deg

Imports5

Imported by8

theorem

card_fiberOver_mul_ramificationIndex_mul_inertiaDeg

L46 ↗

AlgebraicCurve.Place.card_fiberOver_mul_ramificationIndex_mul_inertiaDeg

Source context 7 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.card_fiberOver_mul_ramificationIndex_mul_inertiaDeg {K F' M :
  Type*} [Field K] [Field F'] [Field M]
    [Algebra K F'] [Algebra K M] [Algebra F' M] [IsScalarTower K F' M]
    [FiniteDimensional F' M] [IsGalois F' M] (w : Place K F') (W : Place K M)
    (hW : W.restrict F' = w) :
    (w.fiberOver M).card * (W.ramificationIndex F' * W.inertiaDeg F') = Module.finrank F' M

Module documentation

Place card fiber Over mul ramification Index mul inertia Deg

Declarations

card_fiberOver_mul_ramificationIndex_mul_inertiaDeg