All.lean
Nyll.AlgebraicCurves.Divisors.All
0 declarations indexed from sourceView source ↗
Imports108
- Nyll.AlgebraicCurves.Divisors.Canonical
- Nyll.AlgebraicCurves.Divisors.ClassGroup
- Nyll.AlgebraicCurves.Divisors.ConstantExtension
- Nyll.AlgebraicCurves.Divisors.ConstantExtensionEvaluation
- Nyll.AlgebraicCurves.Divisors.Correspondences
- Nyll.AlgebraicCurves.Divisors.Maps
- Nyll.AlgebraicCurves.Divisors.Pic0Congr
- Nyll.AlgebraicCurves.Divisors.PoleData
- Nyll.AlgebraicCurves.Divisors.Card_effectiveDivisors_mul_eq_sum
- Nyll.AlgebraicCurves.Divisors.Card_effective_sub_isPrincipal_of_finite
- Nyll.AlgebraicCurves.Divisors.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Degree_canonicalDivisor_eq_of_isAlgClosed
- Nyll.AlgebraicCurves.Divisors.Degree_poleDivisor_eq_finrank_adjoin_of_isAlgClosed_of_transcendental
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_comm_of_exchange
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_congr
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_correspondence
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_eq_finrankAlong_smul_correspondence_of_comp_eq
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_eq_ord_norm_and_dlog_norm_eq_traceAlong_pullbackAlong
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_single
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_single_eq_finrankAlong_smul
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_single_of_forall_restrictAlong_eq
- Nyll.AlgebraicCurves.Divisors.Divisor_correspondence_single_one_apply_eq_sum_and_eq_finsum
- Nyll.AlgebraicCurves.Divisors.Divisor_degZero_existsUnique_conorm_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_eq_finrank_adjoin_of_eq_max_neg_ord
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_eq_finrank_adjoin_of_eq_max_ord_sub_algebraMap
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_eq_sum
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_eq_sum_support
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_le_finrank_adjoin_of_eq_max_neg_ord
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_mapDomain_filter_add_degree_mapDomain_filter_eq_degree_of_deg_eq_one
- Nyll.AlgebraicCurves.Divisors.Divisor_degree_nonneg_of_nonneg
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_add
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_algebraMap_pushforward
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_mul
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_pullback
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_pullback_of_isPurelyInseparable
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_single_sub_single
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_zpow_left
- Nyll.AlgebraicCurves.Divisors.Divisor_evalFun_zsmul
- Nyll.AlgebraicCurves.Divisors.Divisor_existsUnique_pullbackConstants_eq_of_forall_smul_eq
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_degZero_ord_eq_mul_of_dvd_ord
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_eq_pow_and_eq_ord_of_inv_smul_D_eq_zero
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_finite_constantField_form_pullbackConstants_eq
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_isPrincipal_degree_eq_zero_forall_mem_support_add_of_surgery
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_pullbackAlong_single_one_eq_sum
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_pullbackAlong_single_restrictAlong_eq_single_add_sum_of_ramificationIndexAlong_eq_one
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_symmValue_rows_kernel_iff
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_torsion_descent_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
- Nyll.AlgebraicCurves.Divisors.Divisor_finrank_adjoin_le_degree_of_eq_max_neg_ord
- Nyll.AlgebraicCurves.Divisors.Divisor_inv_smul_D_eq_inv_smul_D_of_isPrincipal_sub
- Nyll.AlgebraicCurves.Divisors.Divisor_isPrincipal_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Divisor_isPrincipal_of_genus_eq_zero
- Nyll.AlgebraicCurves.Divisors.Divisor_isPrincipal_of_isPrincipal_pullbackConstants_of_isConstantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Divisor_mapDomain_placeReduction_correspondence
- Nyll.AlgebraicCurves.Divisors.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
- Nyll.AlgebraicCurves.Divisors.Divisor_mapDomain_pullbackAlong_eq_and_restrictAlong_eq_of_degZero
- Nyll.AlgebraicCurves.Divisors.Divisor_mem_principal_of_forall_ell_pos_add
- Nyll.AlgebraicCurves.Divisors.Divisor_mem_support_correspondence_single_iff_exists_and_iff_mem_support_correspondence_single
- Nyll.AlgebraicCurves.Divisors.Divisor_ofAlgAut_smul_correspondence_eq_correspondence_ofAlgAut_smul_of_comp_eq_comp
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_liesOver_of_liesOver
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pullbackAlong
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pushforwardAlong_eq_add_of_adjoin_eq_top
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pushforwardAlong_eq_add_of_normFormulaAlong
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pushforwardAlong_eq_pushforwardAlong_pullbackAlong
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pushforwardAlong_eq_sum_ofAlgAut_smul_of_forall_comp_eq
- Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_pushforwardAlong_eq_sum_of_decomposition
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_comp
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_liesOver_of_liesOver
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_pullbackAlong_of_surjective
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_pushforwardAlong
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_single_one
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardAlong_single_one_of_isAlgClosed
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardNormFormula
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardNormFormula_of_finiteDimensional
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardNormFormula_of_isSeparable
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforward_div
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforward_div_of_isSeparable
- Nyll.AlgebraicCurves.Divisors.Divisor_pushforward_pullback_of_finite
- Nyll.AlgebraicCurves.Divisors.Divisor_smul_mem_support_correspondence_single_smul_of_mem_support_of_comp_eq
- Nyll.AlgebraicCurves.Divisors.Divisor_sum_galois_smul_eq_pullback_pushforward
- Nyll.AlgebraicCurves.Divisors.Divisor_support_pullback_subset
- Nyll.AlgebraicCurves.Divisors.Divisor_support_pushforward_subset
- Nyll.AlgebraicCurves.Divisors.Exists_baseChange_correspondence_of_constantFieldExtension
- Nyll.AlgebraicCurves.Divisors.Exists_constantFieldDescent_correspondence
- Nyll.AlgebraicCurves.Divisors.Exists_divisor_eq_floor_and_mul_degree_le_of_min_ord_le
- Nyll.AlgebraicCurves.Divisors.Exists_divisor_eq_max_ord_sub_algebraMap
- Nyll.AlgebraicCurves.Divisors.Exists_divisor_forall_eq_weightFloor
- Nyll.AlgebraicCurves.Divisors.Exists_list_isPrincipal_sub_sum_single_sub_smul_single
- Nyll.AlgebraicCurves.Divisors.Exists_poleDivisor_of_transcendental
- Nyll.AlgebraicCurves.Divisors.Exists_ringEquiv_closure_of_support_correspondence_single_eq_of_essFiniteType
- Nyll.AlgebraicCurves.Divisors.HasCanonicalDivisor_of_isCurveOver
- Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_adjoin_of_transcendental
- Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_finiteDimensional_of_isSeparable
- Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_finiteDimensional_ratFunc
- Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_finiteDimensional_ratFunc_of_isSeparable
- Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_transcendental
- Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_transcendental_of_isSeparable
- Nyll.AlgebraicCurves.Divisors.InstHasCanonicalDivisorRatFuncPerfectField
- Nyll.AlgebraicCurves.Divisors.NormFormulaAlong
- Nyll.AlgebraicCurves.Divisors.NormFormulaAlong_of_separableAlong
- Nyll.AlgebraicCurves.Divisors.Sum_divisors_mul_card_places_lt_of_even
- Nyll.AlgebraicCurves.Divisors.Semilinear.All
- Nyll.AlgebraicCurves.Divisors.Semilinear
- Nyll.AlgebraicCurves.Divisors.Pic0_zsmul_mk
- Nyll.AlgebraicCurves.Divisors.Pic0_mk_eq_zero_iff
- Nyll.AlgebraicCurves.Divisors.Pic0_subsingleton_of_forall_isPrincipal
- Nyll.AlgebraicCurves.Divisors.KummerRootEvaluation
Imported by1
This module has no indexed declarations. Its imports and full source are available here.