All.lean
Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All
0 declarations indexed from sourceView source ↗
Imports112
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Degree_canonicalDivisor_eq_of_riemannRoch
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_add_of_forall_eq_ord
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_canonicalDivisor_eq_genus_of_riemannRoch
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_eq_degree_add_one_sub_genusFF_of_isAlgClosed_of_isSeparable
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_eq_zero_of_degree_neg
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_le_degree_add_ellZero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_le_ell_sub_single_add_deg
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_mapDomain_eq_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_nsmul_eq_card_of_flagAdaptedBasisAt
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_sub_ell_le_degree_sub_degree
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Eq_genusFF_of_forall_ell_sub_ell_eq
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Eq_zero_or_exists_eq_weilOfKaehler_smul_of_mem_omegaSpace
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_canonicalDivisor_genus_riemannRoch
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_flagAdaptedBasisAt_lSpace_nsmul_poleDivisor
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_flagAdaptedBasisAt_lSpace_nsmul_poleDivisor_succ
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_flagAdaptedBasis_lSpace_nsmul_poleDivisor
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_forall_adicValuation_sub_le_of_riemannGenusReachedAt
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_genus_riemannIndex_of_isCurveOver
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_genus_riemannIndex_of_stichtenothGenusExists
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_indexOfSpecialty_mapDomain_eq_zero_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_linearEquiv_regularDifferentials_omegaSpace_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_lSpaceOn_adicValuation_eq_of_riemannGenusReachedAt
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_forall_hasValue_mul_of_exists_not_mem
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_forall_hasValue_zpow_mul_of_ringEquiv_ratFunc
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_not_mem_sub_single_of_ringEquiv_ratFunc
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_isCurveOver_of_essFiniteType
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_smul_single_ord_pos_and_ord_eq_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_pair_forall_ord_add_eq_zero_of_subset_riemannRochSpace
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_riemannGenusReachedAt_of_bounded
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_weilCanonical_riemannRoch
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_weilSmul_eq_of_riemannIndexFormula
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FiniteDimensional_and_finrank_riemannRochSpace_of_ringEquiv_ratFunc
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FiniteDimensional_lSpace
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FiniteDimensional_lSpace_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FiniteDimensional_lSpace_zero_and_ell_zero_eq_one_of_isAlgClosed_of_transcendental
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finite_and_finrank_regularDifferentials_eq_genus
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finite_and_finrank_regularDiffs_eq_genusFF_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finrank_add_card_le_of_forall_exists_mem_riemannRochSpace_hasValue_mul
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finrank_omegaSpace_eq_ell_canonical_sub_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finrank_riemannRochSpace_eq_degree_add_one_of_ringEquiv_ratFunc
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finrank_span_pair_mul_riemannRochSpace_add_finrank
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FunctionFieldRiemannRoch_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FunctionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FunctionFieldRiemannRoch_of_isAlgClosed_of_transcendental
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FunctionFieldRiemannRoch_of_residueTheoremK_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_algEquiv
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_constantFieldExtension_of_finiteDimensional
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_constantFieldExtension_of_finite_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_le_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_le_of_normalForm
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_ratFunc_eq_zero_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_sub_one_eq_of_isSplittingField_of_forall_dvd_ord
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_sub_one_eq_of_isSplittingField_of_forall_dvd_ord_of_natCast_ne_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Genus_eq_genusFF
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Genus_eq_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Genus_eq_zero_of_isPrincipal_single_sub_single
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Genus_ratFunc_eq_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Genus_ratFunc_eq_zero_of_perfectField
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GermToFunctionField_inf_mem_lSpaceOn_inter_placesOf
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GermToFunctionField_mem_lSpaceOn_placesOf
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Germ_mem_lSpaceOn_setOf_exists_centre_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IndexOfSpecialty_eq_ell_sub_of_rankOne_max
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IndexOfSpecialty_eq_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IndexOfSpecialty_eq_zero_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IsRegularLocalRing_stalk_of_lSpaceOn_setOf_centre_zero_subset_range
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IsUnit_det_jetMatrix_iff_span_inf_riemannRochSpace_eq_bot
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpaceOn_setOf_centre_eq_span_integralClosure_mul
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpaceOn_setOf_exists_centre_eq_span_integralClosure
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpace_eq_bot_of_degree_neg
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpace_mapDomain_subset_span_image_lSpace_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpace_nsmul_succ_poleDivisor_le_sup_map_mulLeft_of_ell_eq
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.LSpace_pullbackConstants_eq_span_of_isConstantFieldExtension
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Le_genusFF_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Mem_riemannRochSpace_of_sum_basis_smul_algebraMap_mem_mapDomain
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Mul_mem_lSpace_add
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Mul_mem_lSpace_nsmul_succ_and_reflects_of_poleDivisor
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.NatCast_le_degree_add_degree_of_linearIndependent_of_mem_riemannRochSpace_of_hasValue
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.OmegaSpace_eq_bot_of_degree_canonicalDivisorOf_lt
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.OmegaSpace_finite_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_degree_eq_sub_one_and_ell_eq_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_effective_sub_add_smul_single_mem_principal
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_finset_subset_ell_sub_sum_single_eq_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_forall_hasValue_forall_ord_nonneg
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_injective_forall_forall_mem_ell_sub_sum_single_add_eq_ell_of_lt_card
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_injective_forall_forall_mem_ell_sub_sum_single_eq_one_of_lt_card
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_mem_riemannRochSpace_sub_hasValue_mul_zpow_neg_forall_hasValue
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RiemannGenusBounded_of_indexFinite
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RiemannGenusReachedAt_eq_of_ge
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RiemannGenusReached_of_stichtenothGenusExists
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RiemannIndexFormula_of_genusReached
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.StichtenothGenusExists_of_isCurveOver
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Sum_ordDiff_D_le_two_mul_genusFF_of_isSeparable
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Sum_ord_sub_one_le_two_mul_genusFF_of_isSeparable
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Surjective_and_ker_pi_lSpaceOn_centre_quotient_of_isAffineOpen
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Two_mul_genusFF_sub_one_ge_of_isSplittingField_X_pow_sub_C
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Two_mul_genusFF_sub_two_eq_of_isSeparable_of_tame
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Two_mul_genus_sub_two_eq_of_degree_canonical
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.WeilDifferentialRankOne_of_stichtenothGenusExists
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.WeilOfKaehler_mem_omegaSpace_of_residueTheorem
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.WeilOfKaehler_omegaSpace_le_canonical
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Pic0_subsingleton_of_genusFF_eq_zero
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusOneDivisors
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.OpenBoundary
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_ell_mul_lt_mul_ell_of_degree_pos
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Coefficients_aeval_mem_lSpace_of_isHomogeneous
- Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Tsen
Imported by1
This module has no indexed declarations. Its imports and full source are available here.