AlgebraicCurve.normFormulaAlong_of_separableAlong
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.NormFormulaAlong_of_separableAlong
open AlgebraicCurve
noncomputable sectionLean source · statement
theorem _root_.AlgebraicCurve.normFormulaAlong_of_separableAlong {K F F' : Type*} [Field K] [Field
F] [Field F'] [Algebra K F] [Algebra K F']
(φ : F →ₐ[K] F') [HasPrincipalDivisors K F'] (hfin : FiniteAlong K φ)
(hsep : SeparableAlong K φ) : NormFormulaAlong K φ hfin