All.lean
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.All
0 declarations indexed from sourceView source ↗
Imports134
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AdicCompletionLocalRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RationalLocalization
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.FiberLocalizationQuotient
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Mathlib_RingTheory_RegularLocalRingFlatLocalAscent
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Mathlib_RingTheory_RegularLocalRingQuotientRegular
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Mathlib_RingTheory_SmoothAlgebraOverFieldRegularStalks
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Mathlib_RingTheory_SmoothFieldFiberRegularStalksStandardSmoothReduction
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AdicCompletion_isNoetherianRing_of_isNoetherianRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.AlgHom_injective_of_finite_of_isFractionRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Etale_isReduced_of_isReduced_of_isNoetherianRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_FormallySmooth_exists_formallyUnramified_aeval_and_maximalIdeal_eq_of_finrank_kaehlerDifferential_eq_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_FormallySmooth_of_maximalIdeal_eq_span_of_isSeparable_residueField
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_FormallySmooth_of_maximalIdeal_eq_span_of_perfectField
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_IsSmoothAt_flat_localization_atPrime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Smooth_isIntegrallyClosed_of_isDomain
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Smooth_isReduced_of_isReduced_of_isNoetherianRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Smooth_of_isIntegrallyClosed_of_krullDimLE_one_of_perfectField
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_exists_monoidHom_algebraMap_eq_norm_of_isIntegrallyClosed
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_finite_maximalSpectrum_and_bijective_localization_of_module_finite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_finrank_quotient_span_sub_eq_of_isLocalization_away_of_mul_eq_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_norm_algebraMap_eq_of_isPushout_of_isFractionRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_existsUnique_section_and_ker_eq_span_of_formallySmooth_of_formallyUnramified
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_existsUnique_section_and_ker_eq_span_of_formallyUnramified_of_isLocalization
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_exists_algHom_lift_of_isSmoothAt
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_forall_exists_monic_dvd_eval_of_prime_of_not_associated
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_isLocalRing_of_isDomain_of_moduleFinite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_moduleFinite_localizationAtPrime_of_moduleFinite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_moduleFinite_quotient_span_and_exists_pow_mem_of_isLocalizationAtPrime_of_mem_nonZeroDivisors
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_comap_map_adicCompletion_eq_of_isNoetherianRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_eq_of_le_of_mem_of_mem_minimalPrimes_iff_notMem
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_forall_iff_map_eq_bot_of_forall_away
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_isPrime_le_and_le_and_ringKrullDim_quotient_eq_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_mem_and_mem_and_radical_span_singleton_isPrime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_exists_ne_zero_and_forall_isMaximal_radical_map_isPrime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_add_ringKrullDim_quotient_eq_ringKrullDim_of_finiteType
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_eq_height_under_of_finiteType_of_isIntegral
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_eq_one_of_ne_bot_of_not_isMaximal_of_ringKrullDim_le_two
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_map_quotientMk_span_singleton_add_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_isReduced_quotient_span_singleton_of_forall_mem_associatedPrimes
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_map_comap_eq_self_of_map_includeLeft_eq_map_includeRight
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IntermediateField_isDomain_tensorProduct_of_finrank_le_finrank_adjoin_range
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsDomain_tensorProduct_of_injective_algHom_laurentSeries
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsFractionRing_exists_pow_mul_mem_colon_and_surjective_restrict_of_branchData
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_exists_algebraMap_eq_of_forall_height_eq_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_height_eq_one_of_mem_associatedPrimes
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_isReduced_quotient_span_singleton_of_forall_mem_minimalPrimes
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_mem_minimalPrimes_of_mem_associatedPrimes
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_mem_range_algebraMap_of_forall_height_eq_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_of_isIntegrallyClosedIn_of_faithfulSMul
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_comap_map_adicCompletion_eq
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_eq_bot_of_lt_of_ne_maximalIdeal_of_ringKrullDim_le_two
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_dvd_pow_of_krullDimLE_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_forall_sub_sum_mem_span_pair_of_prime_of_not_associated
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_mem_maximalIdeal_notMem_sq_forall_minimalPrimes_notMem
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_monic_coeff_mem_maximalIdeal_aeval_mem_span_of_pow_mem
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_ringHom_comp_algebraMap_eq_and_ker_eq_span_of_injective_of_finite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_sub_algebraMap_mem_map_maximalIdeal_of_mul_self_sub_mem_of_smul_eq_add
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_exists_subalgebra_coe_eq_isNoetherianRing_isLocalRing_isUnit_iff
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_faithfullyFlat_adicCompletion_maximalIdeal
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_hensel_lift_unique
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isAdicComplete_map_maximalIdeal_quotient
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isAdicComplete_of_module_finite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isRegularLocalRing_of_formallySmooth_of_formallyUnramified_polynomial_of_henselianLocalRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isRegular_of_systemOfParameters
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_length_quotient_map_maximalIdeal_eq_finsum_ramificationIdx_mul_inertiaDeg
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_mem_range_algebraMap_of_flat_of_isLocalHom
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_mk_comp_algebraMap_surjective_of_maximalIdeal_le
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_ringKrullDim_adicCompletion_maximalIdeal_eq
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_two_le_ringKrullDim_adicCompletion_of_two_le
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalization_AtPrime_exists_ringEquiv_adicCompletion_maximalIdeal
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalization_AtPrime_surjective_and_ker_pi_span_mul_quotient_of_moduleFinite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsNoetherianRing_exists_completeOrthogonalIdempotents_forall_connectedSpace_primeSpectrum
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsNoetherianRing_of_ringKrullDim_le_one_of_finiteDimensional_subalgebra
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_quotient_span_singleton_map_of_leftInverse_of_irreducible
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_uniqueFactorizationMonoid_of_ringKrullDim_le_two
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularRing_uniqueFactorizationMonoid_of_isLocalRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_exists_fg_subalgebra_flat_localization_tensorProduct
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_exists_ne_zero_flat_localization_tensorProduct
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_isOpen_setOf_flat_localization_atPrime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_of_isLocalHom_of_isRegularLocalRing_of_ringKrullDim_quotient_eq_zero
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Projective_exists_ideal_fg_forall_tmul_eq_zero_iff_map_eq_bot
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_depth_le_ringKrullDim_quotient_of_mem_associatedPrimes
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_exists_forall_alternatingSum_finrank_cohomology_baseChange_eq_of_flat_complex_of_isLocalRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_exists_notMem_and_free_localizedModule_of_isIntegrallyClosed_of_ringKrullDim_le_one
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_flat_of_comap_maximalIdeal_rTensor_injective
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_flat_of_isLocalHom_of_isNoetherianRing_of_finite_of_tor_one_residueField_isZero
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_flat_of_isLocalHom_of_isNoetherianRing_of_finite_of_tor_one_residueField_isZero_univ
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPolynomial_mem_ideal_iff_forall_map_mem_map_localizationAway
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isAdicComplete_maximalIdeal
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isNoetherianRing_fin
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.MvPowerSeries_isNoetherianRing_of_finite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Polynomial_exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.PrimeSpectrum_apply_eq_apply_of_forall_le_of_connectedSpace
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.PrimeSpectrum_range_comap_eq_zeroLocus_ker_of_isIntegral
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RingHom_existsUnique_eq_smul_kaehlerDifferential_D_of_formallySmooth_of_maximalIdeal_eq_map_sup_span
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RingHom_existsUnique_eq_smul_kaehlerDifferential_D_of_formallySmooth_of_maximalIdeal_eq_span_pair
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RingHom_formallySmooth_and_formallyUnramified_eval2RingHom_of_maximalIdeal_eq_span_pair
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RingTheory_Sequence_IsWeaklyRegular_isZero_tor_one_quotient_ofList
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Subalgebra_isIntegrallyClosed_adjoin_singleton_of_transcendental
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Subalgebra_isNoetherianRing_and_dimensionLEOne_of_isFractionRing_of_finite
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Subalgebra_mem_of_isIntegral_of_fg_of_forall_isPrincipal_maximalIdeal_localization_atPrime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.UniqueFactorizationMonoid_of_isLocalization_away_of_prime
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.exteriorPower_range_map_subtype_eq_maximalIdeal_smul_top
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.isRegularLocalRing_localization_atPrime_mvPolynomial
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.isRegularLocalRing_localization_atPrime_of_etale_of_comap
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.isRegularLocalRing_localization_atPrime_of_isStandardSmooth
- Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.ringKrullDim_le_of_ringHom_isIntegral
Imported by1
This module has no indexed declarations. Its imports and full source are available here.