Module

Place_ord_sub_one_le_ordDiff_D_of_perfectField.lean

Nyll.AlgebraicCurves.Places.Place_ord_sub_one_le_ordDiff_D_of_perfectField

5 declarations indexed from sourceView source ↗

Module documentation

Place ord sub one le ord Diff D of perfect Field

Imports7

Imported by4

theorem

ordDiff_smul_impl

L38 ↗

AlgebraicCurve.Place.ordDiff_smul_impl

Source context 9 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ordDiff_smul_impl [PerfectField K] (x : F)
    [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K
      F)
    {g : F} (hg : g ≠ 0) {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    v.ordDiff (g • ω) = v.ord g + v.ordDiff ω

theorem

ord_pow_nat

L60 ↗

AlgebraicCurves.Places.Proofs.Place_ord_sub_one_le_ordDiff_D_of_perfectField.AlgebraicCurve.Place.ord_pow_nat

Source context 10 commands

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

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

Lean source · statement

theorem ord_pow_nat (v : AlgebraicCurve.Place K F) (t : F) (m : ℕ) :
    v.ord (t ^ m) = (m : ℤ) * v.ord t

theorem

H2_pos

L64 ↗

AlgebraicCurve.Place.H2_pos

Source context 10 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.H2_pos [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K F)
    {f : F} (hD : KaehlerDifferential.D K F f ≠ 0) (hn : 0 ≤ v.ord f) :
    v.ord f - 1 ≤ v.ordDiff (KaehlerDifferential.D K F f)

theorem

H2_impl

L146 ↗

AlgebraicCurves.Places.Proofs.Place_ord_sub_one_le_ordDiff_D_of_perfectField.AlgebraicCurve.Place.H2_impl

Source context 11 commands

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

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

Lean source · statement

theorem H2_impl [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K F)
    {f : F} (hD : KaehlerDifferential.D K F f ≠ 0) :
    v.ord f - 1 ≤ v.ordDiff (KaehlerDifferential.D K F f)

theorem

ord_sub_one_le_ordDiff_D_of_perfectField

L190 ↗

AlgebraicCurve.Place.ord_sub_one_le_ordDiff_D_of_perfectField

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_sub_one_le_ordDiff_D_of_perfectField

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_sub_one_le_ordDiff_D_of_perfectField {K F : Type*} [Field
  K] [Field F] [Algebra K F] [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K
      F) {f : F}
    (hD : KaehlerDifferential.D K F f ≠ 0) :
    v.ord f - 1 ≤ v.ordDiff (KaehlerDifferential.D K F f)

Module documentation

Place ord sub one le ord Diff D of perfect Field

Declarations

ordDiff_smul_impl

ord_pow_nat

H2_pos

H2_impl

ord_sub_one_le_ordDiff_D_of_perfectField