AlgebraicCurve.Place.sum_ramificationIndexAlong_mul_inertiaDegAlong
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndexAlong_mul_inertiaDegAlong
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable sectionLean source · statement
theorem _root_.AlgebraicCurve.Place.sum_ramificationIndexAlong_mul_inertiaDegAlong {K F F' : Type*}
[Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] (φ : F →ₐ[K] F') (hφ :
φ.toRingHom.IsIntegral) [HasPrincipalDivisors K F'] (hfin : FiniteAlong K φ) (hsep :
SeparableAlong K φ) (v : Place K F) : ∑ w ∈ Place.fiberAlong φ hφ v, (w.ramificationIndexAlong φ
: ℤ) * (w.inertiaDegAlong φ hφ : ℤ) = (finrankAlong K φ : ℤ)