Module

Place_ordDiff_eq_ordDifferential_of_perfectField.lean

Nyll.AlgebraicCurves.Places.Place_ordDiff_eq_ordDifferential_of_perfectField

3 declarations indexed from sourceView source ↗

Module documentation

Place ord Diff eq ord Differential of perfect Field

Imports10

Imported by2

theorem

seamAux_coeff_ne_zero

L48 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_eq_ordDifferential_of_perfectField.AlgebraicCurve.Place.seamAux_coeff_ne_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_eq_ordDifferential_of_perfectField
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)

Lean source · statement

theorem seamAux_coeff_ne_zero [v.DCoordGenerates] {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    v.differentialCoeff ω ≠ 0

theorem

seamAux_ordDiff_eq_ordDifferential

L56 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_eq_ordDifferential_of_perfectField.AlgebraicCurve.seamAux_ordDiff_eq_ordDifferential

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_eq_ordDifferential_of_perfectField
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem seamAux_ordDiff_eq_ordDifferential
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    (v : Place K F) (ω : Ω[F⁄K]) :
    v.ordDiff ω = v.ordDifferential ω

theorem

ordDiff_eq_ordDifferential_of_perfectField

L106 ↗

AlgebraicCurve.Place.ordDiff_eq_ordDifferential_of_perfectField

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_eq_ordDifferential_of_perfectField

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ordDiff_eq_ordDifferential_of_perfectField {K F : Type*} [Field
  K]
    [Field F] [Algebra K F] [PerfectField K] [Algebra.EssFiniteType K F]
    [AlgebraicCurve.IsCurveOver K F] (v : AlgebraicCurve.Place K F) (ω : Ω[F⁄K]) :
    v.ordDiff ω = v.ordDifferential ω

Module documentation

Place ord Diff eq ord Differential of perfect Field

Declarations

seamAux_coeff_ne_zero

seamAux_ordDiff_eq_ordDifferential

ordDiff_eq_ordDifferential_of_perfectField