AlgebraicCurve.residueTheorem_of_perfectField
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.ResidueTheorem_of_perfectField
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupDivisor
AlgebraicCurve.Pic0.instModuleZModTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instDistribMulActionTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instSMulTorsion
AlgebraicCurve.SemilinearAut.instMulActionSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instSMulCommClassZModTorsion
AlgebraicCurve.SemilinearAut.instMulSemiringActionSubtypeProdRingAutMemSubgroup
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Divisor.degree_pushforwardAlong AlgebraicCurve.Pic0.coe_degZeroCorrespondence
AlgebraicCurve.Place.mem_fiberAlong AlgebraicCurve.SemilinearAut.toRingAut_inv
AlgebraicCurve.SemilinearAut.smul_def AlgebraicCurve.SemilinearAut.smul_single
AlgebraicCurve.SemilinearAut.smul_toValuationSubring AlgebraicCurve.SemilinearAut.baseAut_inv
AlgebraicCurve.SemilinearAut.baseAut_ofAlgAut AlgebraicCurve.SemilinearAut.toRingAut_ofAlgAut
AlgebraicCurve.SemilinearAut.toRingAut_one AlgebraicCurve.SemilinearAut.deg_smul
AlgebraicCurve.SemilinearAut.degree_smul AlgebraicCurve.SemilinearAut.coe_degZeroSMulHom
AlgebraicCurve.SemilinearAut.baseAut_mul
AlgebraicCurve.SemilinearAut.coe_smulValuationSubringEquiv_apply
AlgebraicCurve.SemilinearAut.baseAut_one AlgebraicCurve.SemilinearAut.ofAlgAut_smul
attribute [-simp] AlgebraicCurve.SemilinearAut.coe_torsion_smul
AlgebraicCurve.SemilinearAut.toRingAut_mul AlgebraicCurve.Divisor.evalFun_zero
AlgebraicCurve.Place.evalAt_one AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
attribute [-simp] AlgebraicCurve.TranscendenceTower.mk.injEq
AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.residueTheorem_of_perfectField
{K F : Type*} [Field K] [PerfectField K]
[Field F] [Algebra K F]
[AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
[∀ w : AlgebraicCurve.Place K F, w.DCoordGenerates]
[Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
[Algebra.IsIntegral (RatFunc K) F] [Module.Finite (RatFunc K) F]
[∀ w : AlgebraicCurve.Place K F, w.FiniteResidue]
[Nontrivial Ω[F⁄K]]
[AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver K (RatFunc K)]
[∀ u : AlgebraicCurve.Place K (RatFunc K), u.FiniteResidue]
[Algebra.IsSeparable (RatFunc K) F]
[AlgebraicCurve.HasCanonicalDivisor (K := K) (F := RatFunc K)]
[Nontrivial Ω[(RatFunc K)⁄K]] [∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates] :
AlgebraicCurve.ResidueTheorem K F