AlgebraicCurve.kaehlerResidueTerm_diagonalHom_eq_zero_of_eq_smul_dCoord
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace KaehlerResidueTerm_diagonalHom_eq_zero_of_eq_smul_dCoord
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.kaehlerResidueTerm_diagonalHom_eq_zero_of_eq_smul_dCoord
{K F : Type*} [Field K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F]
{v : Place K F} [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
{ω : Ω[F⁄K]} {f : F} (hf : f ∈ v.toValuationSubring) (hω : ω = f • v.dCoord)
{g : F} (hg : g ∈ v.toValuationSubring) :
kaehlerResidueTerm ω (diagonalHom K F g) v = 0