AlgebraicCurve.RationalFunctionField.trace_localResidue_placeInfty_X_pow_eq_zero
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_trace_localResidue_placeInfty_X_pow_eq_zero
open _root_.AlgebraicCurves.Places.Rational.Proofs
open _root_.AlgebraicCurve.Place.CanonicalLocalResidueDataKLean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.trace_localResidue_placeInfty_X_pow_eq_zero
(K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
[AlgebraicCurve.HasCanonicalLocalResidueKStar K (RatFunc K)]
[∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates]
[Nontrivial Ω[(RatFunc K)⁄K]]
(n : ℕ) :
Algebra.trace K (AlgebraicCurve.RationalFunctionField.placeInfty K).ResidueField
((AlgebraicCurve.RationalFunctionField.placeInfty K).localResidue
((RatFunc.X : RatFunc K) ^ n
* (AlgebraicCurve.RationalFunctionField.placeInfty K).differentialCoeff
(KaehlerDifferential.D K (RatFunc K) (RatFunc.X : RatFunc K)))) = 0