Module

TraceIntegralAlong_of_separableAlong.lean

Nyll.AlgebraicCurves.FunctionFields.TraceIntegralAlong_of_separableAlong

4 declarations indexed from sourceView source ↗

Module documentation

Trace Integral Along of separable Along

Imports5

Imported by3

theorem

ord_neg_of_not_mem

L37 ↗

AlgebraicCurve.Place.ord_neg_of_not_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TraceIntegralAlong_of_separableAlong
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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_neg_of_not_mem (v : Place K F) {x : F} (hx : x ∉
  v.toValuationSubring) : v.ord x < 0

theorem

eq_of_toValuationSubring_le

L44 ↗

AlgebraicCurves.FunctionFields.Proofs.TraceIntegralAlong_of_separableAlong.AlgebraicCurve.Place.eq_of_toValuationSubring_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TraceIntegralAlong_of_separableAlong
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
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem eq_of_toValuationSubring_le {v v' : Place K F}
    (h : v.toValuationSubring ≤ v'.toValuationSubring) : v' = v

theorem

traceIntegralAlong_of_separableAlong'

L87 ↗

AlgebraicCurves.FunctionFields.Proofs.TraceIntegralAlong_of_separableAlong.AlgebraicCurve.traceIntegralAlong_of_separableAlong'

Source context 6 commands

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

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

Lean source · statement

theorem traceIntegralAlong_of_separableAlong' {F' : Type*} [Field F'] [Algebra K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ) (hsep : SeparableAlong
      K φ) :
    TraceIntegralAlong φ hφ

theorem

traceIntegralAlong_of_separableAlong

L143 ↗

AlgebraicCurve.traceIntegralAlong_of_separableAlong

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TraceIntegralAlong_of_separableAlong
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.FunctionFields.Proofs.TraceIntegralAlong_of_separableAlong.AlgebraicCurve
  in

Lean source · statement

theorem _root_.AlgebraicCurve.traceIntegralAlong_of_separableAlong {K : Type*} {F : Type*} {F' :
  Type*}
    [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ) (hsep : SeparableAlong
      K φ) :
    TraceIntegralAlong φ hφ

Module documentation

Trace Integral Along of separable Along

Declarations

ord_neg_of_not_mem

eq_of_toValuationSubring_le

traceIntegralAlong_of_separableAlong'

traceIntegralAlong_of_separableAlong