AlgebraicCurve.sumRamificationInertia_of_fundamentalIdentity
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SumRamificationInertia_of_fundamentalIdentity
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.sumRamificationInertia_of_fundamentalIdentity
{K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
[IsScalarTower K F F'] [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
[FundamentalIdentity K F F']
(hdeg : ∀ v : Place K F, v.deg ≠ 0) : SumRamificationInertia K F F'