AlgebraicCurve.Place.sum_ramificationIndex_eq_finrank
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_eq_finrank
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.sum_ramificationIndex_eq_finrank {K F F' : Type*} [Field K]
[Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
[FiniteDimensional F F'] [Algebra.IsSeparable F F'] [HasPrincipalDivisors K F'] (v : Place K F)
(hv : v.IsRational) (hrat : ∀ w ∈ v.fiber F', Place.IsRational w) : ∑ w ∈ v.fiber F',
(w.ramificationIndex F : ℤ) = (Module.finrank F F' : ℤ)