Module

Dvd_ord_of_isRegularDiff_dlog.lean

Nyll.AlgebraicCurves.Differentials.Dvd_ord_of_isRegularDiff_dlog

6 declarations indexed from sourceView source ↗

Module documentation

Dvd ord of is Regular Diff dlog

Imports8

Imported by3

theorem

dlog_mul

L43 ↗

AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog.AlgebraicCurve.DlogResidue.dlog_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DlogResidue
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem dlog_mul {a b : F} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b)⁻¹ • D K F (a * b) = a⁻¹ • D K F a + b⁻¹ • D K F b

theorem

dlog_pow

L50 ↗

AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog.AlgebraicCurve.DlogResidue.dlog_pow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DlogResidue
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem dlog_pow {a : F} (ha : a ≠ 0) (m : ℕ) :
    (a ^ m)⁻¹ • D K F (a ^ m) = (m : F) • (a⁻¹ • D K F a)

theorem

dlog_inv

L57 ↗

AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog.AlgebraicCurve.DlogResidue.dlog_inv

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DlogResidue
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem dlog_inv {a : F} (ha : a ≠ 0) :
    (a⁻¹)⁻¹ • D K F a⁻¹ = -(a⁻¹ • D K F a)

theorem

dlog_zpow

L63 ↗

AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog.AlgebraicCurve.DlogResidue.dlog_zpow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DlogResidue
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem dlog_zpow {a : F} (ha : a ≠ 0) (n : ℤ) :
    (a ^ n)⁻¹ • D K F (a ^ n) = (n : F) • (a⁻¹ • D K F a)

theorem

main

L72 ↗

AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog.AlgebraicCurve.DlogResidue.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DlogResidue
open _root_.AlgebraicCurve

Lean source · statement

theorem main
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime]
    [CharP K p] [PerfectField K]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {g : F} (hreg : AlgebraicCurve.IsRegularDiff K F (g⁻¹ • D K F g))
    (v : AlgebraicCurve.Place K F) : (p : ℤ) ∣ v.ord g

theorem

dvd_ord_of_isRegularDiff_dlog

L155 ↗

AlgebraicCurve.dvd_ord_of_isRegularDiff_dlog

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dvd_ord_of_isRegularDiff_dlog
universe u v
open KaehlerDifferential

Lean source · statement

theorem _root_.AlgebraicCurve.dvd_ord_of_isRegularDiff_dlog
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime]
    [CharP K p] [PerfectField K]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {g : F} (hreg : AlgebraicCurve.IsRegularDiff K F (g⁻¹ • D K F g)) :
    ∀ v : AlgebraicCurve.Place K F, (p : ℤ) ∣ v.ord g

Module documentation

Dvd ord of is Regular Diff dlog

Declarations

dlog_mul

dlog_pow

dlog_inv

dlog_zpow

main

dvd_ord_of_isRegularDiff_dlog