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