Module

Place_eq_of_finrank_lt_two_mul_ramificationIndex.lean

Nyll.AlgebraicCurves.Places.Place_eq_of_finrank_lt_two_mul_ramificationIndex

2 declarations indexed from sourceView source ↗

Module documentation

Place eq of finrank lt two mul ramification Index

Imports3

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

place_eq_of_two_mul_le_ramificationIndex

L35 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_finrank_lt_two_mul_ramificationIndex.S09CDZ.place_eq_of_two_mul_le_ramificationIndex

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_finrank_lt_two_mul_ramificationIndex
open AlgebraicCurve
namespace S09CDZ
section Counting
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F
  F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']

Lean source · statement

theorem place_eq_of_two_mul_le_ramificationIndex {U U' : Place K F'} (hres : U'.restrict F =
  U.restrict F) {m : ℕ}
    (hm : Module.finrank F F' < 2 * m) (hU : m ≤ U.ramificationIndex F) (hU' : m ≤
      U'.ramificationIndex F) : U = U'

theorem

eq_of_finrank_lt_two_mul_ramificationIndex

L62 ↗

AlgebraicCurve.Place.eq_of_finrank_lt_two_mul_ramificationIndex

Source context 3 commands