AlgebraicCurve.Place.ord_diffCoeff_D_nonneg_of_perfectField
Source context 25 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_perfectField
attribute [-instance] AlgebraicCurve.Place.instIsPrimeCenter
attribute [-instance] AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance] AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
attribute [-instance]
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance] AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
attribute [-instance] AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
attribute [-instance] AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
attribute [-instance] AlgebraicCurve.Place.instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
attribute [-simp] AlgebraicCurve.Place.mem_fiberOver
attribute [-simp] AlgebraicCurve.Place.fiberEquiv_symm_apply
attribute [-simp] AlgebraicCurve.Place.fiberEquiv_apply
attribute [-simp] AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
attribute [-simp] AlgebraicCurve.Divisor.pushforward_single
attribute [-simp] AlgebraicCurve.Place.coe_restrictInclusion
attribute [-simp] AlgebraicCurve.Place.mem_fiber
attribute [-simp] AlgebraicCurve.Place.restrict_toValuationSubring
attribute [-simp] AlgebraicCurve.Divisor.degree_pushforward
attribute [-simp] AlgebraicCurve.Place.restrictResidueMap_residue
attribute [-simp] AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
attribute [-simp] AlgebraicCurve.Pic0.coe_pullbackDegZeroHomLean source · statement
theorem _root_.AlgebraicCurve.Place.ord_diffCoeff_D_nonneg_of_perfectField {K F : Type*} [Field K]
[Field F] [Algebra K F] [PerfectField K] (x : F)
[FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K
F) {t : F}
(ht : v.ord t = 1) {f : F} (hf : 0 ≤ v.ord f) :
0 ≤ v.ord (AlgebraicCurve.Place.diffCoeff t (KaehlerDifferential.D K F f))