Module

Place_ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint

2 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index Along eq ord sub of restrict Along eq place Of Point

Imports3

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

solution_impl

L34 ↗

AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint.AlgebraicCurve.Place.solution_impl

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.RationalFunctionField
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in

Lean source · statement

theorem AlgebraicCurve.Place.solution_impl
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (φ : RatFunc K →ₐ[K] F) (hφ : φ.toRingHom.IsIntegral)
    (w : AlgebraicCurve.Place K F) (a : K)
    (hwa : w.restrictAlong φ hφ = AlgebraicCurve.RationalFunctionField.placeOfPoint K a) :
    (AlgebraicCurve.Place.ramificationIndexAlong φ w : ℤ) =
      w.ord (φ (RatFunc.X : RatFunc K) - algebraMap K F a)

theorem

ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint

L53 ↗

AlgebraicCurve.Place.ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint

Source context 5 commands