maximalIdeal 📖 | CompOp | 137 mathmath: Irreducible.maximalIdeal_eq_setOf_le_v_coe, ValuationSubring.valuation_lt_one_iff, ValuationSubring.image_maximalIdeal, IsLocalization.AtPrime.liesOver_map_of_liesOver, finrank_CotangentSpace_eq_one_iff, Valuation.mem_maximalIdeal_iff, Ring.KrullDimLE.eq_maximalIdeal_of_isPrime, ker_residue, PowerSeries.zero_weierstrassDiv, PowerSeries.zero_weierstrassMod, PowerSeries.eq_mul_weierstrassDiv_add_weierstrassMod, IsLocalization.AtPrime.mk'_mem_maximal_iff, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, finrank_cotangentSpace_eq_zero, IsDiscreteValuationRing.instIsHausdorffMaximalIdeal, PadicInt.sub_zmodRepr_mem, finrank_quotient_map, PowerSeries.maximalIdeal_eq_span_X, Ring.KrullDimLE.radical_eq_maximalIdeal, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, map_mkQ_eq, maximalIdeal_isPrincipal_of_isDedekindDomain, maximalIdeal_le_jacobson, residue_eq_zero_iff, PadicInt.maximalIdeal_eq_span_p, basisQuotient_repr, Algebra.FormallyUnramified.iff_map_maximalIdeal_eq, IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg, exists_maximalIdeal_pow_le_of_finite_quotient, ResidueField.instLiesOverMaximalIdeal, mem_maximalIdeal, PadicInt.exists_mem_range, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, PowerSeries.smul_weierstrassDiv, Ideal.primeHeight_eq_ringKrullDim_iff, Ring.KrullDimLE.nilradical_eq_maximalIdeal, PowerSeries.IsWeierstrassDivision.unique, maximalIdeal_eq_bot, Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal, IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq, finrank_CotangentSpace_eq_one, finrank_cotangentSpace_eq_zero_iff, residue_def, instHenselianRingMaximalIdeal, DualNumber.maximalIdeal_eq_span_singleton_eps, Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, IsLocalization.AtPrime.comap_maximalIdeal, IsDedekindDomain.primesOverEquivPrimesOver_apply, Valuation.pow_Uniformizer_is_pow_generator, PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassMod, IsLocalization.AtPrime.to_map_mem_maximal_iff, Nat.mem_maximalIdeal_iff, ker_eq_maximalIdeal, IsDiscreteValuationRing.irreducible_iff_uniformizer, instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, PowerSeries.smul_weierstrassMod, LocalSubring.map_maximalIdeal_eq_top_of_isMax, isField_iff_maximalIdeal_eq, Localization.AtPrime.comap_maximalIdeal, Algebra.isUnramifiedAt_iff_map_eq, IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq, instIsHausdorffMaximalIdeal, PadicInt.zmodRepr_spec, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, PowerSeries.weierstrassMod_zero_left, PrimeSpectrum.asIdeal_top, IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk, Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, ValuationSubring.coe_mem_nonunits_iff, IsLocalization.AtPrime.map_eq_maximalIdeal, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal, PowerSeries.isDistinguishedAt_weierstrassDistinguished, finrank_cotangentSpace_le_one_iff, IsLocalization.AtPrime.mem_primesOver_of_isPrime, exists_maximalIdeal_pow_eq_of_principal, maximalIdeal.isMaximal, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, instIsScalarTowerResidueFieldCotangentSpace, Algebra.trace_quotient_mk, Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal, Ideal.isPrime_nat_iff, Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing, PowerSeries.add_weierstrassMod, primesOverFinset_eq, quotient_span_eq_top_iff_span_eq_top, PadicInt.instIsAdicCompleteMaximalIdeal, Irreducible.maximalIdeal_eq, le_maximalIdeal, isMaximal_iff, AlgHom.IsArithFrobAt.isArithFrobAt_localize, isArtinianRing_iff_isNilpotent_maximalIdeal, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, support_of_supportDim_eq_zero, maximalIdeal_primeHeight_eq_ringKrullDim, IsDiscreteValuationRing.TFAE, basisQuotient_apply, trace_quotient_eq_trace_localization_quotient, CotangentSpace.map_eq_top_iff, isOpen_maximalIdeal_pow, PowerSeries.ker_coeff_eq_max_ideal, exists_maximalIdeal_pow_le_of_isArtinianRing_quotient, IsDedekindDomain.primesOverEquivPrimesOver_symm_apply, CotangentSpace.span_image_eq_top_iff, notMem_maximalIdeal, Algebra.FormallyUnramified.map_maximalIdeal, Nat.maximalIdeal_eq_span_two_three, Valuation.IsUniformizer.is_generator, jacobson_eq_maximalIdeal, IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, PadicInt.ker_toZMod, maximalIdeal_height_eq_ringKrullDim, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, Valuation.Uniformizer.is_generator, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, map_mkQ_eq_top, le_maximalIdeal_of_isPrime, IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk, IsLocalization.AtPrime.liesOver_maximalIdeal, Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal, eq_maximalIdeal, finite_quotient_iff, local_hom_TFAE, IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx, PowerSeries.weierstrassDiv_zero_left, Localization.AtPrime.map_eq_maximalIdeal, PowerSeries.add_weierstrassDiv, ringJacobson_eq_maximalIdeal, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, PadicInt.existsUnique_mem_range, Nat.coe_maximalIdeal, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, PadicInt.toZMod_spec, isOpen_maximalIdeal, primesOver_eq, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff
|