theorem
L46 ↗D_ne_zero_of_ord_eq_one
AlgebraicCurve.Place.D_ne_zero_of_ord_eq_one
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_D_ne_zero_of_ord_eq_one
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_pullbackDegZeroHomLean source · statement
theorem _root_.AlgebraicCurve.Place.D_ne_zero_of_ord_eq_one {K F : Type*} [Field K] [Field F]
[Algebra K F] [PerfectField K] (x : F)
[Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
(v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t = 1) :
KaehlerDifferential.D K F t ≠ 0