AlgebraicCurve.Place.derivation_apply_eq_diffCoeff_D_mul
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_derivation_apply_eq_diffCoeff_D_mul
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 AlgebraicCurve KaehlerDifferentialLean source · statement
theorem _root_.AlgebraicCurve.Place.derivation_apply_eq_diffCoeff_D_mul
{K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K] (x : F)
[Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
(v : Place K F) {t : F} (ht : v.ord t = 1) (δ : Derivation K F F) (f : F) :
δ f = Place.diffCoeff t (KaehlerDifferential.D K F f) * δ t