Module

Place_one_le_ramificationIndexAlong.lean

Nyll.AlgebraicCurves.Places.Place_one_le_ramificationIndexAlong

2 declarations indexed from sourceView source ↗

Module documentation

Place one le ramification Index Along

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by2

theorem

solution_impl

L30 ↗

AlgebraicCurves.Places.Proofs.Place_one_le_ramificationIndexAlong.AlgebraicCurve.Place.solution_impl

Source context 3 commands

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

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

Lean source · statement

theorem AlgebraicCurve.Place.solution_impl
    {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : AlgebraicCurve.Place K F') :
    1 ≤ AlgebraicCurve.Place.ramificationIndexAlong φ w

theorem

one_le_ramificationIndexAlong

L40 ↗

AlgebraicCurve.Place.one_le_ramificationIndexAlong

Source context 2 commands