AlgebraicCurve.inv_smul_D_eq_zero_iff_exists_pow_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Inv_smul_D_eq_zero_iff_exists_pow_eq
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.inv_smul_D_eq_zero_iff_exists_pow_eq
{K : Type*} [Field K] [PerfectField K] {F : Type*} [Field F] [Algebra K F]
[Algebra.EssFiniteType K F] [IsCurveOver K F]
(p : ℕ) [Fact p.Prime] [CharP K p]
(f : F) (hf : f ≠ 0) :
f⁻¹ • KaehlerDifferential.D K F f = 0 ↔ ∃ g : F, g ^ p = f