All.lean
Nyll.AlgebraicCurves.Differentials.Residues.All
0 declarations indexed from sourceView source ↗
Imports32
- Nyll.AlgebraicCurves.Differentials.Residues.Basic
- Nyll.AlgebraicCurves.Differentials.Residues.Canonical
- Nyll.AlgebraicCurves.Differentials.Residues.Construction
- Nyll.AlgebraicCurves.Differentials.Residues.FibreIdentity
- Nyll.AlgebraicCurves.Differentials.Residues.ExistsUnique_hasSimpleResidue_of_hasSimplePoleAt
- Nyll.AlgebraicCurves.Differentials.Residues.Exists_linearMap_hasSimpleResidue_ker_eq_regular_range_eq_sum_zero_finrank_corner
- Nyll.AlgebraicCurves.Differentials.Residues.Exists_mem_polarDifferentials_forall_hasSimpleResidue_of_sum_eq_zero
- Nyll.AlgebraicCurves.Differentials.Residues.Exists_place_residue_eq_algebraMap_of_maximalIdeal_eq_span_sup
- Nyll.AlgebraicCurves.Differentials.Residues.Exists_place_ringHom_residue_eq_of_isPrime_le_of_forall_aeval_mem
- Nyll.AlgebraicCurves.Differentials.Residues.FibreResidueIdentityAlong_of_separableAlong_of_dCoordGenerates
- Nyll.AlgebraicCurves.Differentials.Residues.HasCanonicalLocalResidueK
- Nyll.AlgebraicCurves.Differentials.Residues.KaehlerResidueTerm_diagonalHom_eq_zero_of_eq_smul_dCoord
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheoremK_of_isAlgClosed
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheoremK_ratFunc_of_isAlgClosed
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheorem_functionField_of_smoothOfRelativeDimension_one
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheorem_of_isAlgClosed
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheorem_of_perfectField
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheorem_of_residueTheoremK
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheorem_of_residueTheorem_ratFunc_of_residueTraceCompletionCommute
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTheorem_ratFunc_of_perfectField
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTraceCompletionCommute
- Nyll.AlgebraicCurves.Differentials.Residues.ResidueTraceCompletionCommute_v2
- Nyll.AlgebraicCurves.Differentials.Residues.Residue_norm_eq_norm_residue_of_retraction
- Nyll.AlgebraicCurves.Differentials.Residues.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
- Nyll.AlgebraicCurves.Differentials.Residues.Sum_kaehlerResidueTerm_traceFunAlong_mul_eq_sum_kaehlerResidueTerm_traceAlong_smul_pullbackAlong
- Nyll.AlgebraicCurves.Differentials.Residues.TateAgreement
- Nyll.AlgebraicCurves.Differentials.Residues.TateAgreement_v2
- Nyll.AlgebraicCurves.Differentials.Residues.TateChainRule
- Nyll.AlgebraicCurves.Differentials.Residues.TateCommFinite
- Nyll.AlgebraicCurves.Differentials.Residues.TateTraceCompat_of_isSeparable
- Nyll.AlgebraicCurves.Differentials.Residues.WeilKaehlerAgree_of_residueTheorem
- Nyll.AlgebraicCurves.Differentials.Residues.TateTrace
Imported by1
This module has no indexed declarations. Its imports and full source are available here.