Module

FundamentalIdentityAlong.lean

Nyll.AlgebraicCurves.Geometry.FundamentalIdentityAlong

1 declaration indexed from sourceView source ↗

Module documentation

Fundamental Identity Along

Imports2

Imported by5

theorem

fundamentalIdentityAlong

AlgebraicCurve.fundamentalIdentityAlong

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.FundamentalIdentityAlong
open AlgebraicCurve AlgebraicCurve.SemilinearAut
open scoped Pointwise
noncomputable section

Lean source · statement

theorem _root_.AlgebraicCurve.fundamentalIdentityAlong {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 φ) :
  FundamentalIdentityAlong K φ hφ