Module

Place_hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord.lean

Nyll.AlgebraicCurves.Places.Place_hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord

2 declarations indexed from sourceView source ↗

Module documentation

Place has Simple Pole At inv smul D and has Simple Residue int Cast ord

Imports4

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

isRegularAt_of_hasSimpleResidue_zero

L54 ↗

AlgebraicCurves.Places.Proofs.Place_hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord.AlgebraicCurve.Place.isRegularAt_of_hasSimpleResidue_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal AlgebraicCurve.Divisor.mapRestrict_single
  AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
  AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
  AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
  AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in

Lean source · statement

theorem AlgebraicCurve.Place.isRegularAt_of_hasSimpleResidue_zero
    {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) {ω : Ω[F⁄K]}
    (h : v.HasSimpleResidue ω 0) : v.IsRegularAt ω

theorem

hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord

L81 ↗

AlgebraicCurve.Place.hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord

Source context 6 commands