All.lean
Nyll.AlgebraicCurves.Places.All
0 declarations indexed from sourceView source ↗
Imports307
- Nyll.AlgebraicCurves.Places.FinrankPrimePow
- Nyll.AlgebraicCurves.Places.Completion
- Nyll.AlgebraicCurves.Places.Depth
- Nyll.AlgebraicCurves.Places.Evaluation
- Nyll.AlgebraicCurves.Places.EvaluationAlgebra
- Nyll.AlgebraicCurves.Places.OverDVR
- Nyll.AlgebraicCurves.Places.SemilinearValue
- Nyll.AlgebraicCurves.Places.Place_comap_algebraMap_ne_top
- Nyll.AlgebraicCurves.Places.Place_exists_ord_pos
- Nyll.AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
- Nyll.AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
- Nyll.AlgebraicCurves.Places.Place_mem_of_ord_nonneg
- Nyll.AlgebraicCurves.Places.Place_ord_nonneg_of_mem
- Nyll.AlgebraicCurves.Places.AlgEquiv_eq_one_of_forall_smul_place_eq
- Nyll.AlgebraicCurves.Places.Det_taylorCoeff_mul_eq_prod_evalAt_mul_det_jetMatrix
- Nyll.AlgebraicCurves.Places.ExistsUnique_centre_place_of_isProper
- Nyll.AlgebraicCurves.Places.ExistsUnique_pDigits_of_D_ne_zero
- Nyll.AlgebraicCurves.Places.ExistsUnique_pDigits_of_transcendental
- Nyll.AlgebraicCurves.Places.Exists_embedding_place_range_eq_compl_placesOf_of_isSectional
- Nyll.AlgebraicCurves.Places.Exists_finset_forall_not_mem_ramificationIndex_eq_one
- Nyll.AlgebraicCurves.Places.Exists_finset_sum_neg_ord_eq_finrank_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Exists_finset_sum_ord_sub_algebraMap_eq_finrank_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Exists_forall_mem_span_pow_mul_of_forall_ord_nonneg
- Nyll.AlgebraicCurves.Places.Exists_ord_eq_zero_D_eq_smul_D_of_isCurveOver
- Nyll.AlgebraicCurves.Places.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
- Nyll.AlgebraicCurves.Places.Exists_place_evalAt_eq_of_section_of_ker_eq_span
- Nyll.AlgebraicCurves.Places.Exists_place_isRational_forall_evalAt_eq_of_algHom
- Nyll.AlgebraicCurves.Places.Exists_place_notMem_ord_neg_and_forall_ord_eq_one
- Nyll.AlgebraicCurves.Places.Exists_place_over_of_simple_root_along
- Nyll.AlgebraicCurves.Places.Exists_place_range_stalk_eq
- Nyll.AlgebraicCurves.Places.Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing
- Nyll.AlgebraicCurves.Places.Finite_setOf_ord_ne_zero_of_finiteDimensional
- Nyll.AlgebraicCurves.Places.Finrank_adjoin_le_mul_natCard_place_ord_sub_algebraMap_pos_of_forall_ord_le
- Nyll.AlgebraicCurves.Places.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
- Nyll.AlgebraicCurves.Places.Finsum_ramificationIndexAlong_sub_one_eq
- Nyll.AlgebraicCurves.Places.Finsum_ramificationIndex_ratFunc_sub_one_eq_of_tame
- Nyll.AlgebraicCurves.Places.IsIntegral_adjoin_of_forall_mem_toValuationSubring
- Nyll.AlgebraicCurves.Places.IsIntegral_adjoin_of_forall_ord_nonneg
- Nyll.AlgebraicCurves.Places.Ker_productMap_eq_of_placeEquiv_restrictAlong
- Nyll.AlgebraicCurves.Places.Mem_integralClosure_iff_forall_place
- Nyll.AlgebraicCurves.Places.Mul_apply_eq_mul_sub_min_ord_of_eq_floor_of_mul_degree_eq_finrank
- Nyll.AlgebraicCurves.Places.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
- Nyll.AlgebraicCurves.Places.Nonempty_place_of_transcendental_of_finiteDimensional
- Nyll.AlgebraicCurves.Places.PDigits_existsUnique
- Nyll.AlgebraicCurves.Places.Place_CanonicalLocalResidueDataK_res_differentialCoeff_D_mul_inv_eq_one
- Nyll.AlgebraicCurves.Places.Place_CanonicalLocalResidueDataK_res_differentialCoeff_D_mul_pow_inv_eq_zero_of_surjective_algebraMap
- Nyll.AlgebraicCurves.Places.Place_D_ne_zero_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_D_ne_zero_of_ord_ne_zero
- Nyll.AlgebraicCurves.Places.Place_adicValuation_isRankOneDiscrete
- Nyll.AlgebraicCurves.Places.Place_adicValuation_isTrivialOn
- Nyll.AlgebraicCurves.Places.Place_algebraMap_coeff_neg_one_eq_localResidue_mul_differentialCoeff_D
- Nyll.AlgebraicCurves.Places.Place_canonicalLocalResidueDataK_eq
- Nyll.AlgebraicCurves.Places.Place_card_fiberAlong_le_finrankAlong_and_iff
- Nyll.AlgebraicCurves.Places.Place_card_fiberOver_mul_ramificationIndex_mul_inertiaDeg
- Nyll.AlgebraicCurves.Places.Place_card_fiber_eq_finrank_adjoin_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_count_normalizedFactors_span_singleton
- Nyll.AlgebraicCurves.Places.Place_deg_eq_one_iff_surjective_algebraMap_residueField
- Nyll.AlgebraicCurves.Places.Place_deg_eq_one_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_deg_ne_zero_of_finiteDimensional_adjoin
- Nyll.AlgebraicCurves.Places.Place_derivation_apply_eq_diffCoeff_D_mul
- Nyll.AlgebraicCurves.Places.Place_derivative_evalEval_evalAt_ne_zero_of_ord_sub_eq_one_of_forall_evalAt_ne
- Nyll.AlgebraicCurves.Places.Place_derivative_evalEval_evalAt_ne_zero_of_ord_sub_eq_one_of_forall_evalAt_ne_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_diffCoeff_smul_D_eq
- Nyll.AlgebraicCurves.Places.Place_diffCoeff_smul_D_eq_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_diffCoeff_smul_D_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_diffCoeff_smul_D_of_ord_ne_zero
- Nyll.AlgebraicCurves.Places.Place_eq_map_mk_taylorCoeff_of_evalEval_C_add_X_eq_zero
- Nyll.AlgebraicCurves.Places.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
- Nyll.AlgebraicCurves.Places.Place_eq_of_comap_toValuationSubring_eq_of_isRational
- Nyll.AlgebraicCurves.Places.Place_eq_of_finrank_lt_two_mul_ramificationIndex
- Nyll.AlgebraicCurves.Places.Place_eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain
- Nyll.AlgebraicCurves.Places.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_eq_of_toValuationSubring_le
- Nyll.AlgebraicCurves.Places.Place_eq_ord_of_addHom_of_nonneg_iff
- Nyll.AlgebraicCurves.Places.Place_eq_taylorCoeff_inv_of_forall_sum_antidiagonal_eq
- Nyll.AlgebraicCurves.Places.Place_evalAt_algebraMap
- Nyll.AlgebraicCurves.Places.Place_evalAt_algebraMap_eq_evalAt_restrict
- Nyll.AlgebraicCurves.Places.Place_evalAt_congr
- Nyll.AlgebraicCurves.Places.Place_evalAt_eq_zero_iff_one_le_ord
- Nyll.AlgebraicCurves.Places.Place_evalAt_inv
- Nyll.AlgebraicCurves.Places.Place_evalAt_map_eq_of_comap_eq
- Nyll.AlgebraicCurves.Places.Place_evalAt_mul
- Nyll.AlgebraicCurves.Places.Place_evalAt_ne_zero
- Nyll.AlgebraicCurves.Places.Place_evalAt_norm_eq_prod_fiber
- Nyll.AlgebraicCurves.Places.Place_evalAt_smul_smul_eq_baseAut_evalAt
- Nyll.AlgebraicCurves.Places.Place_evalAt_trace_eq_sum_fiber
- Nyll.AlgebraicCurves.Places.Place_evalAt_zpow
- Nyll.AlgebraicCurves.Places.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero
- Nyll.AlgebraicCurves.Places.Place_eval_leadingCoeff_ne_zero_of_forall_mem_toValuationSubring
- Nyll.AlgebraicCurves.Places.Place_existsUnique_forall_mem_iff_adjoin_sup_of_isAlgebraic_of_forall_exists_sub_mem
- Nyll.AlgebraicCurves.Places.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
- Nyll.AlgebraicCurves.Places.Place_existsUnique_valuation_sub_lt_one_of_constantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_exists_algEquiv_smul_eq_of_restrict_eq
- Nyll.AlgebraicCurves.Places.Place_exists_algHom_laurentSeries_of_deg_eq_one
- Nyll.AlgebraicCurves.Places.Place_exists_algHom_laurentSeries_order_eq_ord
- Nyll.AlgebraicCurves.Places.Place_exists_comap_algebraMap_eq_of_constantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_exists_comap_algebraMap_eq_of_constantFieldExtension_of_deg_eq_one_of_isAlgebraic
- Nyll.AlgebraicCurves.Places.Place_exists_comap_algebraMap_eq_of_constantFieldExtension_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_exists_comap_eq_toValuationSubring
- Nyll.AlgebraicCurves.Places.Place_exists_comap_toValuationSubring_eq_of_ne_top_of_isAlgebraic
- Nyll.AlgebraicCurves.Places.Place_exists_eq_smul_D_of_ord_ne_zero
- Nyll.AlgebraicCurves.Places.Place_exists_eq_smul_dCoord_and_uniformizer_pow_mul_mem_of_cartierLaws
- Nyll.AlgebraicCurves.Places.Place_exists_equiv_comap_eq_and_ord_eq_and_deg_eq_of_ringEquiv
- Nyll.AlgebraicCurves.Places.Place_exists_finite_constantField_form_fiberConstants_eq_singleton
- Nyll.AlgebraicCurves.Places.Place_exists_finset_forall_notMem_toValuationSubring_or_ord_sub_algebraMap_pos_imp_mem
- Nyll.AlgebraicCurves.Places.Place_exists_finset_forall_ord_sub_algebraMap_eq_one_of_ord_pos
- Nyll.AlgebraicCurves.Places.Place_exists_forall_adicValuation_sub_eq
- Nyll.AlgebraicCurves.Places.Place_exists_forall_adicValuation_sub_le
- Nyll.AlgebraicCurves.Places.Place_exists_forall_mem_and_mem_nonunits_iff_not_isUnit_of_isLocalRing
- Nyll.AlgebraicCurves.Places.Place_exists_forall_mem_hasValue
- Nyll.AlgebraicCurves.Places.Place_exists_forall_mem_iff_adjoin_sup_of_linearDisjoint
- Nyll.AlgebraicCurves.Places.Place_exists_forall_ord_eq
- Nyll.AlgebraicCurves.Places.Place_exists_forall_ord_eq_finset
- Nyll.AlgebraicCurves.Places.Place_exists_forgetConstants_restrict_eq_of_isConstantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_exists_gram_denominator_of_mulTable
- Nyll.AlgebraicCurves.Places.Place_exists_integralClosureAt_of_ord_fiber_nonneg
- Nyll.AlgebraicCurves.Places.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
- Nyll.AlgebraicCurves.Places.Place_exists_irreducible_dCoord_eq_D_and_hasPoleOrderLE_iff
- Nyll.AlgebraicCurves.Places.Place_exists_isIntegral_adjoin_and_ord_eq_one_and_forall_ord_eq_zero
- Nyll.AlgebraicCurves.Places.Place_exists_isIntegral_adjoin_eq_top_ord_sub_algebraMap_eq_one
- Nyll.AlgebraicCurves.Places.Place_exists_not_mem_and_forall_ne_mem
- Nyll.AlgebraicCurves.Places.Place_exists_not_mem_range_and_forall_ne_ord_nonneg
- Nyll.AlgebraicCurves.Places.Place_exists_of_isPrime_over_valuationSubring
- Nyll.AlgebraicCurves.Places.Place_exists_of_orderMap
- Nyll.AlgebraicCurves.Places.Place_exists_of_valuationSubring
- Nyll.AlgebraicCurves.Places.Place_exists_of_valuationSubring_of_finiteDimensional
- Nyll.AlgebraicCurves.Places.Place_exists_of_valuationSubring_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_exists_ord_algebraMap_eq_mul_ord
- Nyll.AlgebraicCurves.Places.Place_exists_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_exists_ord_eq_one_of_ord_sum_eq_one
- Nyll.AlgebraicCurves.Places.Place_exists_ord_neg_of_transcendental
- Nyll.AlgebraicCurves.Places.Place_exists_ord_sub_algebraMap_pos_of_transcendental
- Nyll.AlgebraicCurves.Places.Place_exists_place_comap_algebraMap_eq_of_finite
- Nyll.AlgebraicCurves.Places.Place_exists_place_comap_eq_and_ord_eq_mul_ord_of_forall_smul_maximalIdeal_map_eq_pow
- Nyll.AlgebraicCurves.Places.Place_exists_restrictAlong_eq_of_finiteDimensional_fieldRange
- Nyll.AlgebraicCurves.Places.Place_exists_restrict_eq
- Nyll.AlgebraicCurves.Places.Place_exists_sub_algebraMap_evalAt_eq_mul_of_derivative_evalEval_ne_zero
- Nyll.AlgebraicCurves.Places.Place_exists_sub_algebraMap_mem_maximalIdeal
- Nyll.AlgebraicCurves.Places.Place_exists_sub_algebraMap_mem_nonunits_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap
- Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap_of_ne_top
- Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap_ringHom
- Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap_ringHom_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_exists_uniformizing_separating_form
- Nyll.AlgebraicCurves.Places.Place_exists_valuationSubring_algHom_apply_eq_forall_mem_iff
- Nyll.AlgebraicCurves.Places.Place_finite_residueField_of_finiteDimensional
- Nyll.AlgebraicCurves.Places.Place_finite_setOf_card_fiberAlong_ne_finrankAlong
- Nyll.AlgebraicCurves.Places.Place_finite_setOf_deg_eq
- Nyll.AlgebraicCurves.Places.Place_finite_setOf_not_mem_toValuationSubring_or_evalAt_mem
- Nyll.AlgebraicCurves.Places.Place_forall_localSubring_iff_forall_localization
- Nyll.AlgebraicCurves.Places.Place_forall_lt_taylorCoeff_eq_zero_iff_le_ord
- Nyll.AlgebraicCurves.Places.Place_hasPoleOrderLE_one_inv_smul_D_and_hasLogResidue_intCast_ord
- Nyll.AlgebraicCurves.Places.Place_hasSimplePoleAt_inv_smul_D_and_hasSimpleResidue_intCast_ord
- Nyll.AlgebraicCurves.Places.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
- Nyll.AlgebraicCurves.Places.Place_hasValue_norm_along_of_separableAlong
- Nyll.AlgebraicCurves.Places.Place_hasValue_smul_iff
- Nyll.AlgebraicCurves.Places.Place_inertiaDegAlong_comp
- Nyll.AlgebraicCurves.Places.Place_inertiaDegAlong_eq_one_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_inertiaDeg_eq_inertiaDeg_fiberCenter
- Nyll.AlgebraicCurves.Places.Place_inertiaDeg_eq_of_restrict_eq
- Nyll.AlgebraicCurves.Places.Place_inertiaDeg_eq_one_of_isRational
- Nyll.AlgebraicCurves.Places.Place_inertiaDeg_pos
- Nyll.AlgebraicCurves.Places.Place_inertiaDeg_pos_of_finiteDimensional
- Nyll.AlgebraicCurves.Places.Place_isDedekindDomain_iInf_toSubring_and_isMaximal_iff_of_finset_nonempty
- Nyll.AlgebraicCurves.Places.Place_isRational_iff_deg_eq_one
- Nyll.AlgebraicCurves.Places.Place_isRational_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_isRational_of_range_stalk_section_eq
- Nyll.AlgebraicCurves.Places.Place_isRegularAt_D_algebraMap_of_forall_algebraMap_mem_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_mul_pullbackAlong_restrictAlong
- Nyll.AlgebraicCurves.Places.Place_isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_of_cartierLaws_of_finiteDimensional
- Nyll.AlgebraicCurves.Places.Place_isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_smul_pullbackAlong_of_algEquiv
- Nyll.AlgebraicCurves.Places.Place_isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_sum_traceAlong_of_separableAlong_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_isSeparable_adjoin_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_isSeparable_adjoin_of_ord_ne_zero_of_cast_natAbs_ne_zero
- Nyll.AlgebraicCurves.Places.Place_isSeparable_adjoin_of_ord_ne_zero_of_cast_natAbs_ne_zero_divisorClassGroup
- Nyll.AlgebraicCurves.Places.Place_kaehlerD_ne_zero_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_le_ord_iff_mem_pow_fiberCenter
- Nyll.AlgebraicCurves.Places.Place_mapDomain_filter_apply_le_ord_of_sections
- Nyll.AlgebraicCurves.Places.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
- Nyll.AlgebraicCurves.Places.Place_mem_and_evalAt_trace_eq_sum_ramificationIndexAlong_smul_evalAt
- Nyll.AlgebraicCurves.Places.Place_mem_range_algebraMap_of_forall_ord_eq_zero
- Nyll.AlgebraicCurves.Places.Place_mem_range_algebraMap_of_forall_ord_eq_zero_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Place_mem_toValuationSubring_iff_map_mem_of_forall_place_eq_of_testFamily
- Nyll.AlgebraicCurves.Places.Place_mem_toValuationSubring_of_evalEval_eq_zero_of_eval_leadingCoeff_ne_zero
- Nyll.AlgebraicCurves.Places.Place_mem_toValuationSubring_of_isIntegral_adjoin
- Nyll.AlgebraicCurves.Places.Place_min_ord_le_ord_add
- Nyll.AlgebraicCurves.Places.Place_mk_mem_maximalIdeal_iff
- Nyll.AlgebraicCurves.Places.Place_mk_taylorCoeff_aeval
- Nyll.AlgebraicCurves.Places.Place_mk_taylorCoeff_eq_C_add_X
- Nyll.AlgebraicCurves.Places.Place_mk_taylorCoeff_evalEval
- Nyll.AlgebraicCurves.Places.Place_module_finite_residueField_restrict
- Nyll.AlgebraicCurves.Places.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
- Nyll.AlgebraicCurves.Places.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
- Nyll.AlgebraicCurves.Places.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
- Nyll.AlgebraicCurves.Places.Place_neg_le_ord_trace_of_forall_le_ord
- Nyll.AlgebraicCurves.Places.Place_neg_le_ord_trace_of_forall_le_ord_of_isCurveOver
- Nyll.AlgebraicCurves.Places.Place_neg_le_ord_trace_of_forall_le_ord_sub_pred
- Nyll.AlgebraicCurves.Places.Place_neg_log_valuation_fiberCenter_eq_ord
- Nyll.AlgebraicCurves.Places.Place_one_le_ramificationIndexAlong
- Nyll.AlgebraicCurves.Places.Place_ordDiff_D_eq_ord_sub_algebraMap_sub_one_of_cast_natAbs_ne_zero
- Nyll.AlgebraicCurves.Places.Place_ordDiff_D_eq_ord_sub_one
- Nyll.AlgebraicCurves.Places.Place_ordDiff_D_nonneg
- Nyll.AlgebraicCurves.Places.Place_ordDiff_eq_ordDifferential
- Nyll.AlgebraicCurves.Places.Place_ordDiff_eq_ordDifferential_of_perfectField
- Nyll.AlgebraicCurves.Places.Place_ordDiff_eq_ord_diffCoeff
- Nyll.AlgebraicCurves.Places.Place_ordDiff_pullbackDiff_of_natCast_ramificationIndexAlong_ne_zero
- Nyll.AlgebraicCurves.Places.Place_ordDiff_smul
- Nyll.AlgebraicCurves.Places.Place_ordDiff_smul_D_nonneg_of_ord_pow_six_mul_pow_four_mul_sub_1728_pow_three_nonneg
- Nyll.AlgebraicCurves.Places.Place_ordDiff_smul_of_perfectField
- Nyll.AlgebraicCurves.Places.Place_ordDiff_zero
- Nyll.AlgebraicCurves.Places.Place_ordDiff_zero_of_perfectField
- Nyll.AlgebraicCurves.Places.Place_ordDifferential_D_eq_zero_of_constantFieldExtension_of_forall_mem
- Nyll.AlgebraicCurves.Places.Place_ord_add_eq_of_lt
- Nyll.AlgebraicCurves.Places.Place_ord_algebraMap
- Nyll.AlgebraicCurves.Places.Place_ord_algebraMap_eq_mul_ord_of_constant_extension
- Nyll.AlgebraicCurves.Places.Place_ord_algebraMap_eq_ord_of_comap_eq_of_isSeparable_of_adjoin_eq_top
- Nyll.AlgebraicCurves.Places.Place_ord_diffCoeff_D_nonneg
- Nyll.AlgebraicCurves.Places.Place_ord_diffCoeff_D_nonneg_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_ord_diffCoeff_D_nonneg_of_perfectField
- Nyll.AlgebraicCurves.Places.Place_ord_eq_and_sum_deg_eq_deg_of_comap_eq_of_linearDisjoint
- Nyll.AlgebraicCurves.Places.Place_ord_eq_neg_log_of_valuationSubring_eq
- Nyll.AlgebraicCurves.Places.Place_ord_eq_zero_of_isAlgebraic
- Nyll.AlgebraicCurves.Places.Place_ord_eq_zero_of_isIntegral_adjoin
- Nyll.AlgebraicCurves.Places.Place_ord_eq_zero_of_not_mem_of_eval_monic_eq_zero_of_coeff_eq_aeval_inv_div
- Nyll.AlgebraicCurves.Places.Place_ord_natCast
- Nyll.AlgebraicCurves.Places.Place_ord_nonneg_of_D_eq_smul_D_of_ord_eq_one
- Nyll.AlgebraicCurves.Places.Place_ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg
- Nyll.AlgebraicCurves.Places.Place_ord_norm_eq_sum_fiberOver
- Nyll.AlgebraicCurves.Places.Place_ord_norm_eq_sum_fiberOver_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_ord_norm_eq_zero_of_forall_fiber
- Nyll.AlgebraicCurves.Places.Place_ord_norm_eq_zero_of_forall_fiber_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_ord_norm_sub_eq_ord_eval
- Nyll.AlgebraicCurves.Places.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
- Nyll.AlgebraicCurves.Places.Place_ord_smul_of_ne_zero
- Nyll.AlgebraicCurves.Places.Place_ord_sub_algebraMap_evalAt_eq_one_of_derivative_evalEval_ne_zero_of_ord_sub_algebraMap_evalAt_eq_one
- Nyll.AlgebraicCurves.Places.Place_ord_sub_one_le_ordDiff_D_of_perfectField
- Nyll.AlgebraicCurves.Places.Place_ord_sum_algebraMap_mul_le_ord_of_linearIndependent_of_constantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_pairwiseDisjoint_fiber
- Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_comp
- Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_of_pow_eq_of_isCoprime_ord
- Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
- Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
- Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_ord_sub_of_restrictAlong_eq_placeOfPoint
- Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_smul
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_div_gcd_natAbs_ord_of_isSplittingField_X_pow_sub_C
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_of_restrict_eq
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_one_of_forall_dvd_ord
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_one_of_forall_dvd_ord_of_isSeparable
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_ramificationIdx_fiberCenter
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_forgetConstants_eq_one_of_isConstantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_ramificationIndex_mul_inertiaDeg_mul_natCard_stabilizer_eq_natCard_stabilizer
- Nyll.AlgebraicCurves.Places.Place_residueField_eq_compositum_of_isConstantFieldExtension
- Nyll.AlgebraicCurves.Places.Place_restrictAlong_algEquiv_eq_ofAlgAut_symm_smul
- Nyll.AlgebraicCurves.Places.Place_restrictAlong_congrEquiv_and_existsUnique_iff
- Nyll.AlgebraicCurves.Places.Place_restrictAlong_eq_smul_of_forall_eq_inv_smul_pow
- Nyll.AlgebraicCurves.Places.Place_restrictAlong_inclusion_of_le_of_le
- Nyll.AlgebraicCurves.Places.Place_restrictAlong_restrictAlong
- Nyll.AlgebraicCurves.Places.Place_restrictAlong_surjective
- Nyll.AlgebraicCurves.Places.Place_restrict_eq_of_forall_mem
- Nyll.AlgebraicCurves.Places.Place_restrict_ofAlgAut_smul
- Nyll.AlgebraicCurves.Places.Place_smul_eq_and_sub_mem_nonunits_of_smul_eq_of_comap_eq
- Nyll.AlgebraicCurves.Places.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
- Nyll.AlgebraicCurves.Places.Place_smul_restrictAlong
- Nyll.AlgebraicCurves.Places.Place_sub_one_add_pow_sub_one_le_ordDiff_D_of_isGalois
- Nyll.AlgebraicCurves.Places.Place_subfieldClosure_range_union_eq_top_of_restrictAlong_injOn
- Nyll.AlgebraicCurves.Places.Place_sum_deg_fiberConstants_eq_deg_of_isCurveOver
- Nyll.AlgebraicCurves.Places.Place_sum_fiber_ord_eq_finrank
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndexAlong_mul_inertiaDegAlong
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_eq_finrank
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_bifiber_defect
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_exchange_add
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_fiberOver
- Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_le_finrank
- Nyll.AlgebraicCurves.Places.Place_sum_ramification_evalAt_eq
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_add
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_algebraMap
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_eq_evalAt_mul_inv_pow_of_forall_taylorCoeff_eq_zero
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_mul
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_ord_ne_zero
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_smul
- Nyll.AlgebraicCurves.Places.Place_taylorCoeff_succ_eq_taylorCoeff_taylorRem_one
- Nyll.AlgebraicCurves.Places.Place_taylorRem_add
- Nyll.AlgebraicCurves.Places.Place_taylorRem_eq_mul_inv_pow_of_forall_taylorCoeff_eq_zero
- Nyll.AlgebraicCurves.Places.Place_taylorRem_mem_toValuationSubring
- Nyll.AlgebraicCurves.Places.Place_taylorRem_smul
- Nyll.AlgebraicCurves.Places.Place_taylorRem_succ_eq_taylorRem_taylorRem_one
- Nyll.AlgebraicCurves.Places.Place_trace_eq_zero_or_neg_add_one_le_ord_trace_of_forall_le_ord
- Nyll.AlgebraicCurves.Places.Place_transcendental_of_ord_ne_zero
- Nyll.AlgebraicCurves.Places.PlacesOf_preimage_eq_preimage_restrictAlong_placesOf
- Nyll.AlgebraicCurves.Places.PlacesOf_preimage_subset_preimage_restrictAlong_placesOf
- Nyll.AlgebraicCurves.Places.PlacesOf_union_eq_univ_of_sup_eq_top
- Nyll.AlgebraicCurves.Places.Preimage_restrictAlong_placesOf_subset_placesOf_preimage
- Nyll.AlgebraicCurves.Places.Six_mul_degree_eq_mul_finrank_of_forall_eq_weightFloor_of_ord_eq_three_two
- Nyll.AlgebraicCurves.Places.SumRamificationInertia_of_fundamentalIdentity
- Nyll.AlgebraicCurves.Places.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
- Nyll.AlgebraicCurves.Places.Transcendental_and_finiteDimensional_adjoin_of_valuations
- Nyll.AlgebraicCurves.Places.Rational.All
- Nyll.AlgebraicCurves.Places.Taylor.All
- Nyll.AlgebraicCurves.Places.Taylor
- Nyll.AlgebraicCurves.Places.Value
- Nyll.AlgebraicCurves.Places.SemilinearEvaluation
- Nyll.AlgebraicCurves.Places.Place_ord_eq_zero_of_evalAt_ne_zero
- Nyll.AlgebraicCurves.Places.LocalUnramifiedRamification
Imported by1
This module has no indexed declarations. Its imports and full source are available here.