All.lean
Nyll.AlgebraicCurves.Valuations.All
0 declarations indexed from sourceView source ↗
Imports91
- Nyll.AlgebraicCurves.Valuations.AdicCompletion
- Nyll.AlgebraicCurves.Valuations.Algebra_IsStandardSmoothOfRelativeDimension_isDiscreteValuationRing_localization_atPrime
- Nyll.AlgebraicCurves.Valuations.Algebra_exists_adjoin_ne_zero_mul_forall_valuationSubring_mem
- Nyll.AlgebraicCurves.Valuations.Ideal_height_eq_one_of_isDiscreteValuationRing_localization_atPrime
- Nyll.AlgebraicCurves.Valuations.Ideal_span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing
- Nyll.AlgebraicCurves.Valuations.IsAlgClosed_exists_valuationSubring_ringHom_retraction
- Nyll.AlgebraicCurves.Valuations.IsAlgClosed_exists_valuationSubring_ringHom_retraction_forall_valuation_eq_one
- Nyll.AlgebraicCurves.Valuations.IsDiscreteValuationRing_adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete
- Nyll.AlgebraicCurves.Valuations.IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring
- Nyll.AlgebraicCurves.Valuations.IsDiscreteValuationRing_forall_valuationSubring_eq_and_forall_exists_sub_mem_nonunits_of_primesOver_integralClosure_eq_singleton
- Nyll.AlgebraicCurves.Valuations.IsDiscreteValuationRing_primesOver_integralClosure_eq_range_of_finrank_le_sum_inertiaDeg
- Nyll.AlgebraicCurves.Valuations.IsIntegrallyClosed_exists_valuationSubring_mem_iff_and_nonunits_iff_of_height_eq_one
- Nyll.AlgebraicCurves.Valuations.IsIntegrallyClosed_isDiscreteValuationRing_localization_of_mem_associatedPrimes
- Nyll.AlgebraicCurves.Valuations.IsIntegrallyClosed_isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes
- Nyll.AlgebraicCurves.Valuations.IsLocalRing_exists_ofList_pair_eq_maximalIdeal_and_isRegular_of_isDiscreteValuationRing_quotient
- Nyll.AlgebraicCurves.Valuations.IsLocalRing_exists_valuationSubring_isDiscreteValuationRing_dominates
- Nyll.AlgebraicCurves.Valuations.IsLocalRing_finite_and_natCard_ringHom_valuationSubring_eq_length_quotient_map_maximalIdeal
- Nyll.AlgebraicCurves.Valuations.Localization_AtPrime_isDiscreteValuationRing_of_height_eq_one
- Nyll.AlgebraicCurves.Valuations.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
- Nyll.AlgebraicCurves.Valuations.PadicInt_natCard_quotient_range_eq_pow_valuation_det
- Nyll.AlgebraicCurves.Valuations.ValuationRing_exists_ne_zero_forall_smul_eq_zero_of_module_finite
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_aeval_div_eq_aeval_div_add_aeval_inv_div
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_aeval_div_eq_aeval_div_add_inv_pow_mul_add_aeval_inv
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_eq_aeval_div_of_forall_valuationSubring_mem_of_eq_sum_mul
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_eq_mul_pow_finrank_and_adjoin_simple_eq_of_forall_valuationSubring_eq
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_eq_units_mul_prod_sub_algebraMap_of_notMem_map_maximalIdeal
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_eq_valuationSubringAtPrime_of_forall_algebraMap_mem
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_finset_forall_exists_mem_span_mul_eq_of_intermediateField_le
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_forall_mem_and_sub_mem_nonunits
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_intermediateField_finiteDimensional_henselianLocalRing_comap_of_henselianLocalRing
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_layer_isDiscreteValuationRing_of_finite_of_isAlgebraic_of_irreducible
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_le_forall_mem_iff_apply_mem
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_map_subtype_eq_C_inv_mul_and_map_residue_ne_zero
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_mul_pow_inv_mem_of_finiteDimensional_adjoin
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_padicInt_forall_apply_eq_pow_appr_mul_of_pow_eq_of_residue_eq
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_polynomial_map_residue_ne_zero_eval_mul_mem
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_pow_eq_unit_mul_zpow_of_isAlgebraic_of_isNoetherianRing
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_ringHom_extend_of_isAlgClosed
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_root_mem_of_monic
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_smul_mem_of_transcendental_residue
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_sub_mem_nonunits_of_finrank_le_card
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_unit_apply_eq_mul_of_mem_iff_apply_mem_of_rankOne
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_valuation_mul_eq_one_of_finrank_le_card
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_valuation_mul_eq_one_of_forall_sup_eq_top
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_faithfullyFlat_and_isIntegral_of_henselianLocalRing_comap
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_finite_primeSpectrum_of_ringKrullDim_lt_top
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_finrank_residueField_le_and_forall_mul_inv_mem_and_forall_eq_of_gauss
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_finsum_ramificationIdx_mul_inertiaDeg_eq_finrank
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_henselianLocalRing_of_isAlgClosed
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_isAlgClosed_completion_of_mulArchimedean_valueGroup
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_isAlgClosed_residueField_of_isAlgClosed
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_isDiscreteValuationRing_of_algebraMap_mem_of_finite
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_isPrincipalIdealRing_of_finiteDimensional_adjoin
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_isUnit_norm_aeval_derivative_minpoly
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_mem_adjoin_singleton_of_isIntegral_of_separable_minpoly
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_mem_and_sub_mem_maximalIdeal_of_gaussPresentation_of_coe_eq_of_coeffMap_residue_comp_eq
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_mem_iff_exists_not_dvd_of_prime_of_forall_mem_maximalIdeal_iff_dvd
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_mem_of_forall_mem_iff_of_subset
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_mulArchimedean_valueGroup_of_isAlgebraic_of_valuation_natCast_lt_one
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_natDegree_map_eq_card_roots_of_splits
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_residueValuationSubring_valuation_lt_one_iff
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_le_ringKrullDim_comap_add_trdeg
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_sum_finrank_residueField_le_finrank_of_forall_mem_iff
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_tensorProduct_exists_primitive_factor
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_toSubring_eq_integralClosure_and_finite_and_isDiscreteValuationRing_of_henselian
- Nyll.AlgebraicCurves.Valuations.Valuation_exists_le_one_iff_exists_eq_mk_of_forall_exists_eq_pow_mul
- Nyll.AlgebraicCurves.Valuations.Valued_exists_forall_v_sub_eq_one_and_v_det_eq_one_of_v_sub_sum_div_lt_one
- Nyll.AlgebraicCurves.Valuations.Valued_exists_mulVec_add_eq_of_v_det_eq_one
- Nyll.AlgebraicCurves.Valuations.Valued_isClosed_submodule_of_finiteDimensional_of_isClosed_subfield
- Nyll.AlgebraicCurves.Valuations.Valued_multipliable_one_add_of_tendsto_cofinite_zero
- Nyll.AlgebraicCurves.Valuations.Valued_v_prod_sub_one_sub_sum_sub_le_of_forall_v_sub_sub_mul_sub_le
- Nyll.AlgebraicCurves.Valuations.Valued_v_tprod_eq_finsetProd_of_forall_not_mem_v_eq_one
- Nyll.AlgebraicCurves.Valuations.WittVector_exists_valuationSubring_residueField_equiv_of_isAlgebraic
- Nyll.AlgebraicCurves.Valuations.existsUnique_valuationSubring_of_pow_eq_mul
- Nyll.AlgebraicCurves.Valuations.ValuationSubring_ResidueValuationSubring
- Nyll.AlgebraicCurves.Valuations.Valuation_CompletionAlgebra
- Nyll.AlgebraicCurves.Valuations.FinitelyGeneratedMixedCharacteristic
- Nyll.AlgebraicCurves.Valuations.FinitelyGeneratedValuationDetection
- Nyll.AlgebraicCurves.Valuations.FinitelyGeneratedMovingValuation
Imported by1
This module has no indexed declarations. Its imports and full source are available here.