AlgebraicCurve.Place.hasPoleOrderLE_one_inv_smul_D_and_hasLogResidue_intCast_ord
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_hasPoleOrderLE_one_inv_smul_D_and_hasLogResidue_intCast_ord
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
attribute [-simp] 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 AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.hasPoleOrderLE_one_inv_smul_D_and_hasLogResidue_intCast_ord
{K : Type*} [Field K] [IsAlgClosed K] {F : Type*} [Field F] [Algebra K F]
[Algebra.EssFiniteType K F] [IsCurveOver K F]
(f : F) (hf : f ≠ 0) (v : Place K F) :
v.HasPoleOrderLE 1 (f⁻¹ • KaehlerDifferential.D K F f) ∧
v.HasLogResidue (f⁻¹ • KaehlerDifferential.D K F f) ((v.ord f : ℤ) : K)