Maps

📁 Source: Mathlib/RingTheory/Ideal/Maps.lean

Statistics

Metric	Count
Definitions idealMap, comap, giMapComap, map, mapHom, orderEmbeddingOfSurjective, piOrderIso, relIsoOfBijective, relIsoOfSurjective, annihilator, idealComapOrderIso, ker, liftOfRightInverse, liftOfRightInverseAux, liftOfSurjective, annihilator	16
Theorems coe_ideal_map, comap_ker, ker_coe, ker_coe_equiv, idealMap_apply_coe, ker_algebraMap_eq_bot, comap_bijective, comap_piEvalRingHom, map_bijective, map_of_surjective_of_ker_le, comap, comap, apply_coe_mem_map, apply_mem_of_equiv_iff, coe_comap, coe_piOrderIso_apply, coe_piOrderIso_symm_apply, coe_restrictScalars, comap_bot_le_of_injective, comap_bot_of_injective, comap_coe, comap_comap, comap_comapₐ, comap_eq_top_iff, comap_finsetInf, comap_iInf, comap_id, comap_idₐ, comap_inf, comap_injective_of_surjective, comap_isMaximal_of_equiv, comap_isMaximal_of_surjective, comap_isPrime, comap_le_comap_iff_of_surjective, comap_le_iff_le_map, comap_le_map_of_inv_on, comap_le_map_of_inverse, comap_map_comap, comap_map_eq_self_iff_of_isPrime, comap_map_eq_self_of_isMaximal, comap_map_of_bijective, comap_map_of_surjective, comap_map_of_surjective', comap_mono, comap_ne_top, comap_of_equiv, comap_radical, comap_sInf, comap_sInf', comap_symm, comap_top, disjoint_map_primeCompl_iff_comap_le, exists_ideal_comap_le_prime, gc_map_comap, instIsPrincipalIdealRingForallOfFinite, instIsTwoSidedComap, instIsTwoSidedMapRingHomOfRingHomSurjective, isMaximal_comap_iff_of_bijective, isMaximal_iff_of_bijective, isMaximal_map_iff_of_bijective, ker_le_comap, le_comap_map, le_comap_mul, le_comap_of_map_le, le_comap_pow, le_comap_sup, le_map_of_comap_le_of_surjective, mapHom_apply, map_bot, map_coe, map_comap_eq_self_of_equiv, map_comap_le, map_comap_map, map_comap_of_equiv, map_comap_of_surjective, map_eq_bot_iff_le_ker, map_eq_bot_iff_of_injective, map_eq_iff_sup_ker_eq_of_surjective, map_eq_submodule_map, map_eq_top_or_isMaximal_of_surjective, map_evalRingHom_pi, map_iInf_comap_of_surjective, map_iSup, map_iSup_comap_of_surjective, map_id, map_idₐ, map_inf_comap_of_surjective, map_inf_le, map_isMaximal_of_equiv, map_isPrime_of_equiv, map_isPrime_of_surjective, map_le_comap_of_inv_on, map_le_comap_of_inverse, map_le_iff_le_comap, map_le_of_le_comap, map_map, map_mapₐ, map_mono, map_mul, map_ne_bot_of_ne_bot, map_of_equiv, map_pointwise_smul, map_pow, map_radical_le, map_radical_of_surjective, map_sInf, map_sSup, map_span, map_sup, map_sup_comap_of_surjective, map_surjective_of_surjective, map_symm, map_top, mem_comap, mem_image_of_mem_map_of_surjective, mem_map_iff_of_surjective, mem_map_of_equiv, mem_map_of_mem, ne_bot_of_map_ne_bot, restrictScalars_mul, smul_restrictScalars, smul_top_eq_map, symm_apply_mem_of_equiv_iff, annihilator_eq, annihilator_le_of_injective, annihilator_le_of_surjective, annihilator_dfinsupp, annihilator_eq_bot, annihilator_eq_top_iff, annihilator_finsupp, annihilator_pi, annihilator_prod, comap_annihilator, mem_annihilator, ker_ringHom, idealComapOrderIso_apply, idealComapOrderIso_symm_apply, comap_ker, eq_liftOfRightInverse, eq_liftOfSurjective, injective_iff_ker_eq_bot, instIsTwoSidedKer, ker_coe_equiv, ker_coe_toRingHom, ker_comp_of_injective, ker_eq, ker_eq_bot_iff_eq_zero, ker_eq_comap_bot, ker_eq_top_of_subsingleton, ker_equiv, ker_equiv_comp, ker_evalRingHom, ker_isMaximal_of_surjective, ker_isPrime, ker_ne_top, ker_rangeRestrict, ker_rangeSRestrict, liftOfRightInverseAux_comp_apply, liftOfRightInverse_comp, liftOfRightInverse_comp_apply, liftOfSurjective_comp, liftOfSurjective_comp_apply, mem_ker, one_notMem_ker, sub_mem_ker_iff, annihilator_bot, annihilator_eq_top_iff, annihilator_iSup, annihilator_mono, annihilator_mul, annihilator_smul, annihilator_span, annihilator_span_singleton, annihilator_top, le_annihilator_iff, mem_annihilator, mem_annihilator', mem_annihilator_span, mem_annihilator_span_singleton, mul_annihilator, element_smul_restrictScalars, instIsPrincipalMapRingHom, instIsTwoSidedAnnihilator	183
Total	199

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ideal_map 📖	mathematical	—	Ideal.map AlgHom funLike RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom AlgHomClass.toRingHomClass algHomClass	—	—
comap_ker 📖	mathematical	—	Ideal.comap AlgHom funLike AlgHomClass.toRingHomClass algHomClass RingHom.ker comp	—	RingHom.comap_ker
ker_coe 📖	mathematical	—	RingHom.ker AlgHom funLike AlgHomClass.toRingHomClass algHomClass RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass RingHomClass.toRingHom	—	AlgHomClass.toRingHomClass algHomClass
ker_coe_equiv 📖	mathematical	—	RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass RingHomClass.toRingHom AlgEquiv AlgEquiv.instFunLike AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	RingHom.ker_coe_equiv

Algebra

Definitions

Name	Category	Theorems
idealMap 📖	CompOp	3 math math: idealMap_eq_ofEq_comp_toLocalized₀, idealMap_isLocalizedModule, idealMap_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealMap_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule SetLike.instMembership Submodule.setLike Submodule.restrictScalars Semiring.toModule toSMul IsScalarTower.right Ideal.map RingHom RingHom.instFunLike algebraMap DFunLike.coe LinearMap RingHom.id Ideal Submodule.addCommMonoid Submodule.module Submodule.module' LinearMap.instFunLike idealMap	—	IsScalarTower.right

FaithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_algebraMap_eq_bot 📖	mathematical	—	RingHom.ker RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass algebraMap Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Ideal.ext RingHom.instRingHomClass

Ideal

Definitions

Name	Category	Theorems
comap 📖	CompOp	189 math math: comap_fiberIsoOfBijectiveResidueField_apply, comap_bot_le_of_injective, exists_comap_galRestrict_eq, comap_comapₐ, IsLocalization.minimalPrimes_map, le_comap_of_map_le, comap_inf, ramificationIdx_comap_eq, RingEquiv.idealComapOrderIso_apply, algebraMap_quotient_injective, Localization.AtPrime.mapPiEvalRingHom_bijective, coeff_zero_mem_comap_of_root_mem_of_eval_mem, comap_jacobson_of_surjective, exists_comap_eq_of_mem_minimalPrimes_of_injective, comap_cotangentIdeal, comap_symm, inertiaDeg_comap_eq, comap_map_eq_self_of_faithfullyFlat, map_mk_comap_factor, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, IsLocalization.AtPrime.comap_map_eq_map, comap_finsetInf, comap_isMaximal_of_equiv, comap_map_eq_self_iff_of_isPrime, Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule, comap_idₐ, comap_iInf, IsLocalization.comap_map_of_isPrime_disjoint, comap_le_map_of_inverse, AlgebraicGeometry.stalkwise_SpecMap_iff, injective_quotient_le_comap_map, comap_of_equiv, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, RingHom.comap_ker, map_inf_comap_of_surjective, IsLocalization.isMaximal_iff_isMaximal_disjoint, map_le_comap_of_inv_on, comap_sInf', relNorm_le_comap, map_mk_comap_factorPow, Module.comap_annihilator, comap_eq_top_iff, PrimeSpectrum.specComap_asIdeal, AddValuation.comap_supp, disjoint_map_primeCompl_iff_comap_le, Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt, AlgHom.comap_ker, IsMaximal.comap_bijective, comp_quotientMap_eq_of_comp_eq, Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, IsLocalization.AtPrime.comap_maximalIdeal, IsPrime.comap, IsMaximal.comap_piEvalRingHom, comap_isMaximal_of_surjective, IsLocalization.isPrime_iff_isPrime_disjoint, Localization.localRingHom_id, IsLocalization.bot_lt_comap_prime, IsLocalization.map_comap, IsLocalization.AtPrime.liesOver_comap_of_liesOver, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgHom.IsArithFrobAt.comap_eq, RingOfIntegers.not_dvd_exponent_iff, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, comap_bot_of_injective, Localization.AtPrime.comap_maximalIdeal, IsLocalization.minimalPrimes_comap, image_comap_zeroLocus_eq_zeroLocus_comap, Valuation.comap_supp, IsIntegralClosure.comap_lt_comap, PrimeSpectrum.sigmaToPi_asIdeal, le_comap_of_ramificationIdx_ne_zero, comap_mono, Algebra.WeaklyQuasiFiniteAt.comap_algEquiv, comap_sInf, AlgHom.IsArithFrobAt.le_comap, map_le_comap_of_inverse, exists_ideal_over_prime_of_isIntegral_of_isDomain, comap_le_comap_iff_of_surjective, Polynomial.isMaximal_comap_C_of_isJacobsonRing, exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff, map_sup_comap_of_surjective, RingHom.surjective_localRingHom_of_surjective, IsLocalization.isLocalization_isLocalization_atPrime_isLocalization, PrimeSpectrum.mem_range_comap_iff, comap_liesOver, RingEquiv.height_comap, comap_map_quotientMk, minimalPrimes_eq_comap, comap_surjective_of_faithfullyFlat, Polynomial.isMaximal_comap_C_of_isMaximal, map_iSup_comap_of_surjective, ker_le_comap, pointwise_smul_eq_comap, map_le_iff_le_comap, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, comap_map_of_surjective, under_def, coe_comap, comap_map_mk, PrimeSpectrum.closure_image_comap_zeroLocus, comap_lt_comap_of_integral_mem_sdiff, AlgebraicGeometry.stalkwise_Spec_map_iff, comap_map_of_bijective, isMaximal_comap_of_isIntegral_of_isMaximal, RingHom.IsIntegral.quotient, comap_map_eq_self_of_isMaximal, IsLocalization.disjoint_comap_iff, IsPRadical.comap_pNilradical, RingHom.ker_eq_comap_bot, IntegralClosure.comap_lt_comap, map_comap_of_equiv, map_symm, comap_map_comap, minimal_primes_comap_of_surjective, Algebra.Generators.ker_comp_eq_sup, le_comap_map, comap_minimalPrimes_eq_of_surjective, map_comap_eq_self_of_equiv, IsRadical.comap, comap_le_map_of_inv_on, IsLocalization.AtPrime.comap_map_of_isMaximal, le_comap_pow, isMaximal_comap_iff_of_bijective, IsLocalization.comap_map_of_isPrimary_disjoint, PrimeSpectrum.comap_asIdeal, map_iInf_comap_of_surjective, IsDedekindDomain.primesOverEquivPrimesOver_symm_apply, image_specComap_zeroLocus_eq_zeroLocus_comap, comap_isPrime, exists_coeff_ne_zero_mem_comap_of_root_mem, minimalPrimes_comap_subset, spanNorm_le_comap, exists_ideal_over_maximal_of_isIntegral, Polynomial.map_under_lt_comap_of_quasiFiniteAt, span_singleton_absNorm, map_comap_natCastRingHom_int, comap_top, quotientMap_injective, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, Localization.le_comap_primeCompl_iff, idealFactorsFunOfQuotHom_coe_coe, IsLocalization.isLocalization_atPrime_localization_atPrime, IsPrimary.comap, Algebra.IsIntegral.quotient, map_comap_map, le_comap_sup, comap_map_of_surjective', comap_fiberIsoOfBijectiveResidueField_symm, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, map_comap_le, CharP.quotient_iff_le_ker_natCast, comap_radical, comap_coe, quotient_mk_maps_eq, IsLocalization.ideal_eq_iInf_comap_map_away, isIntegral_quotientMap_iff, coeff_zero_mem_comap_of_root_mem, IsLocalization.orderIsoOfPrime_apply_coe, IsLocalization.primeHeight_comap, Ring.le_comap_jacobson, mem_comap, le_comap_mul, exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem, Algebra.QuasiFiniteAt.comap_algEquiv, RingHom.surjectiveOnStalks_iff_forall_maximal, IsLocalRing.local_hom_TFAE, instIsTwoSidedComap, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, isMaximal_comap_of_isIntegral_of_isMaximal', comap_injective_of_surjective, map_comap_of_surjective, comap_id, comap_eq_of_scalar_tower_quotient, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, comap_lt_comap_of_root_mem_sdiff, IsLocalization.height_comap, gc_map_comap, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, comap_jacobson, relNorm_comap_algEquiv, comap_le_iff_le_map, RingHom.surjective_localRingHom_iff, le_comap_pow_ramificationIdx, comap_comap, Polynomial.isIntegral_isLocalization_polynomial_quotient
giMapComap 📖	CompOp	—
map 📖	CompOp	340 math math: Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt, IsDedekindDomain.differentIdeal_dvd_map_differentIdeal, Polynomial.ker_mapRingHom, IsLocalization.map_radical, Algebra.idealMap_eq_ofEq_comp_toLocalized₀, DoubleQuot.liftSupQuotQuotMkₐ_toRingHom, IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply, IsLocalization.AtPrime.liesOver_map_of_liesOver, IsLocalization.minimalPrimes_map, map_eq_top_iff_of_ker_le, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk, NumberField.isCoprime_differentIdeal_of_isCoprime_discr, map_ofList, differentIdeal_eq_differentIdeal_mul_differentIdeal, PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, exists_mem_span_singleton_map_residueField_eq, smul_top_eq_map, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, MvPolynomial.ker_map, IsMaximal.map_bijective, coe_smul_primesOver_mk_eq_map_galRestrict, DividedPowers.IsDPMorphism.ideal_comp, Polynomial.fiberEquivQuotient_tmul, map_fst_prod, PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime, comap_symm, DoubleQuot.coe_quotQuotMkₐ, Submodule.IsPrincipal.map_ringHom, IsLocalRing.finrank_quotient_map, comap_map_eq_self_of_faithfullyFlat, quotient_map_C_eq_zero, map_mk_comap_factor, PowerBasis.quotientEquivQuotientMinpolyMap_apply, Factors.fact_ramificationIdx_neZero, map_spanIntNorm, QuotientMapQuotient.isNoetherian, IsLocalization.AtPrime.comap_map_eq_map, DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv, map_under_le_under_map, height_eq_height_add_of_liesOver_of_hasGoingDown, Quotient.tower_quotient_map_quotient, map_eq_top_or_isMaximal_of_surjective, DoubleQuot.quotQuotEquivComm_symmₐ, liesOver_iff_dvd_map, FractionalIdeal.extendedHomₐ_coeIdeal_eq_map, comap_map_eq_self_iff_of_isPrime, spanIntNorm_localization, isPrime_map_of_isLocalizationAtPrime, jacobson_bot_polynomial_le_sInf_map_maximal, mem_map_of_mem, Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, IsLocalRing.basisQuotient_repr, Algebra.FormallyUnramified.iff_map_maximalIdeal_eq, IsLocalization.comap_map_of_isPrime_disjoint, map_mul, FG.map, comap_le_map_of_inverse, IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg, injective_quotient_le_comap_map, Quotient.algebraMap_quotient_map_quotient, DoubleQuot.quotQuotEquivComm_comp_quotQuotMk, DoubleQuot.quotQuotEquivComm_quotQuotMk, Algebra.Generators.map_toComp_ker, map_id, powQuotSuccInclusion_apply_coe, map_inf_comap_of_surjective, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, IsLocalization.mapFrameHom_apply, IsLocalization.map_inf, DoubleQuot.quotQuotToQuotSupₐ_toRingHom, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, Algebra.Generators.map_ofComp_ker, IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, PowerSeries.map_constantCoeff_le_self_of_X_mem, map_relNorm, map_le_comap_of_inv_on, localized'_eq_map, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, IsLocalization.AtPrime.exists_algebraMap_quot_eq_of_mem_quot, map_includeRight_eq, Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal, DividedPowers.isSubDPIdeal_map, map_mk_comap_factorPow, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, map_mk_eq_bot_of_le, Algebra.TensorProduct.map_ker, height_le_height_add_of_liesOver, height_le_height_add_one_of_mem, Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt, MvPolynomial.quotient_map_C_eq_zero, Polynomial.height_map_C, IsMaximal.map_of_surjective_of_ker_le, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, under_map_of_isLocalizationAtPrime, map_span, Factors.isScalarTower, DividedPowers.isDPMorphism_iff, IsLocalization.algebraMap_mem_map_algebraMap_iff, IsDedekindDomain.primesOverEquivPrimesOver_apply, quotientToQuotientRangePowQuotSucc_mk, mem_map_of_equiv, AdjoinRoot.quotEquivQuotMap_apply, le_pow_ramificationIdx, IsLocalization.height_map_of_disjoint, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, map_radical_of_surjective, mem_quotient_iff_mem, le_map_of_comap_le_of_surjective, IsLocalization.map_comap, IsHausdorff.map_algebraMap_iff, FractionalIdeal.extended_coeIdeal_eq_map, DoubleQuot.ker_quotQuotMk, map_eq_bot_iff_of_injective, DoubleQuot.coe_quotQuotEquivQuotSupₐ, LocalSubring.map_maximalIdeal_eq_top_of_isMax, isPrime_map_quotientMk_of_isPrime, ramificationIdx_map_eq, symm_apply_mem_of_equiv_iff, map_evalRingHom_pi, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, Algebra.isUnramifiedAt_iff_map_eq, relNorm_algebraMap', IsLocalization.isPrime_of_isPrime_disjoint, map_quotient_self, IsLocalization.mk'_mem_map_algebraMap_iff, spanRank_map_le, spanFinrank_map_le_of_fg, quotAdjoinEquivQuotMap_apply_mk, PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, quotientToQuotientRangePowQuotSucc_surjective, localized₀_eq_restrictScalars_map, RingEquiv.idealComapOrderIso_symm_apply, Valuation.supp_quot, ideal_prod_eq, map_snd_prod, map_le_comap_of_inverse, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, relNorm_algebraMap, Rat.HeightOneSpectrum.natGenerator_dvd_iff, finrank_quotient_map, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.mem_map_C_iff, map_sup_comap_of_surjective, map_radical_le, map_bot, DoubleQuot.quotQuotMkₐ_toRingHom, ker_quotient_lift, PrimeSpectrum.mem_range_comap_iff, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, map_sup, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, comap_map_quotientMk, DividedPowers.DPMorphism.ideal_comp, DividedPowers.isDPMorphism_def, map_eq_top_iff, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, map_iSup_comap_of_surjective, Quotient.factor_ker, map_le_iff_le_comap, IsLocalization.AtPrime.map_eq_maximalIdeal, DoubleQuot.ker_quotLeftToQuotSup, comap_map_of_surjective, Factors.liesOver, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, Polynomial.contentIdeal_map_eq_map_contentIdeal, IsLocalization.AtPrime.isMaximal_map, KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly, comap_map_mk, Rat.HeightOneSpectrum.span_natGenerator, Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, isPrime_map_C_of_isPrime, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, apply_mem_of_equiv_iff, quotientToQuotientRangePowQuotSucc_injective, Algebra.idealMap_isLocalizedModule, minimalPrimes_map_of_surjective, AlgHom.coe_ideal_map, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, apply_coe_mem_map, mem_map_C_iff, PowerSeries.fg_iff_of_isPrime, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, comap_map_of_bijective, Algebra.trace_quotient_mk, RingEquiv.height_map, polynomialQuotientEquivQuotientPolynomial_symm_mk, map_isPrime_of_equiv, map_of_equiv, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map, IsLocalization.orderIsoOfPrime_symm_apply_coe, map_map, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul, map_eq_submodule_map, MvPolynomial.ker_mapAlgHom, comap_map_eq_self_of_isMaximal, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, Factors.finrank_pow_ramificationIdx, DividedPowers.Quotient.isDPMorphism, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, Algebra.weaklyQuasiFiniteAt_iff, rank_pow_quot_aux, map_comap_of_equiv, smul_restrictScalars, mem_primesOver_iff_mem_normalizedFactors, map_sInf, map_symm, coe_smul_primesOver_eq_map_galRestrict, map_algebraMap_eq_finset_prod_pow, rank_pow_quot, comap_map_comap, map_height_le_one_of_mem_minimalPrimes, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, instIsPrincipalMapRingHom, Algebra.Generators.ker_comp_eq_sup, IsLocalization.ker_map, le_comap_map, mem_quotient_iff_mem_sup, map_comap_eq_self_of_equiv, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.coe_quotQuotToQuotSupₐ, map_isMaximal_of_equiv, IsLocalRing.basisQuotient_apply, trace_quotient_eq_trace_localization_quotient, map_eq_iff_sup_ker_eq_of_surjective, map_mapₐ, ker_quotientMap_mk, comap_le_map_of_inv_on, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', powQuotSuccInclusion_injective, IsLocalization.AtPrime.comap_map_of_isMaximal, Algebra.TensorProduct.lTensor_ker, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, map_inf_le, IsLocalization.comap_map_of_isPrimary_disjoint, mem_map_iff_of_surjective, Algebra.trace_quotient_eq_of_isDedekindDomain, map_iInf_comap_of_surjective, Algebra.mem_ideal_map_adjoin, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, instIsTwoSidedMapRingHomOfRingHomSurjective, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk, map_surjective_of_surjective, IsDedekindDomain.ramificationIdx_eq_factors_count, IsLocalization.isMaximal_of_isMaximal_disjoint, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, Polynomial.map_under_lt_comap_of_quasiFiniteAt, map_sSup, map_isPrime_of_surjective, map_comap_natCastRingHom_int, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, AdjoinRoot.quotEquivQuotMap_symm_apply, isDomain_map_C_quotient, Polynomial.IsWeaklyEisensteinAt.map, map_mono, height_le_height_add_encard_of_subset, Algebra.FormallyUnramified.map_maximalIdeal, DividedPowers.Quotient.dpow_apply, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, DividedPowers.isSubDPIdeal_map_of_isSubDPIdeal, map_top, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, Factors.finiteDimensional_quotient_pow, map_le_of_le_comap, le_pow_of_le_ramificationIdx, isMaximal_map_iff_of_bijective, idealFactorsFunOfQuotHom_coe_coe, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, IsDedekindDomain.ramificationIdx_eq_multiplicity, IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, DoubleQuot.quotQuotEquivComm_mk_mk, map_comap_map, Factors.isPrime, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk, comap_map_of_surjective', DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, map_equiv_liesOver, height_le_height_add_spanFinrank_of_le, map_idₐ, under_map_eq_map_under, DoubleQuot.coe_quotQuotEquivCommₐ, map_comap_le, map_prodComm_prod, polynomialQuotientEquivQuotientPolynomial_map_mk, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap, quotient_mk_maps_eq, IsLocalization.ideal_eq_iInf_comap_map_away, DoubleQuot.quotQuotEquivQuotOfLE_symm_mk, IsLocalization.mem_map_algebraMap_iff, inertiaDeg_map_eq, absNorm_algebraMap, map_pointwise_smul, quotientToQuotientRangePowQuotSuccAux_mk, relNorm_map_algEquiv, isPrime_map_C_iff_isPrime, map_jacobson_of_bijective, IsLocalization.AtPrime.isPrime_map_of_liesOver, Factors.piQuotientEquiv_mk, map_coe, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, IsLocalRing.local_hom_TFAE, IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx, Quotient.mk_smul_mk_quotient_map_quotient, map_pow, Algebra.idealMap_apply_coe, AddValuation.supp_quot, Localization.AtPrime.map_eq_maximalIdeal, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_includeLeft_eq, map_iSup, map_jacobson_of_surjective, Algebra.TensorProduct.rTensor_ker, map_comap_of_surjective, IsLocalization.liesOver_of_isPrime_of_disjoint, mapHom_apply, DoubleQuot.coe_liftSupQuotQuotMkₐ, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk, gc_map_comap, map_prime_of_equiv, pointwise_smul_def, ramificationIdx_map_self_eq_one, DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk, comap_le_iff_le_map, map_eq_bot_iff_le_ker, DoubleQuot.quotQuotEquivComm_symm, Factors.piQuotientEquiv_map, comap_map_eq_map_adjoin_of_coprime_conductor, DoubleQuot.quotQuotEquivComm_algebraMap, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff
mapHom 📖	CompOp	1 math math: mapHom_apply
orderEmbeddingOfSurjective 📖	CompOp	—
piOrderIso 📖	CompOp	2 math math: coe_piOrderIso_symm_apply, coe_piOrderIso_apply
relIsoOfBijective 📖	CompOp	—
relIsoOfSurjective 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_coe_mem_map 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map DFunLike.coe	—	mem_map_of_mem
apply_mem_of_equiv_iff 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike DFunLike.coe	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass comap_symm mem_comap RingEquiv.symm_apply_apply
coe_comap 📖	mathematical	—	SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap Set.preimage DFunLike.coe	—	—
coe_piOrderIso_apply 📖	mathematical	—	SetLike.coe Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike DFunLike.coe RelIso Ideal Pi.semiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Pi.hasLe RelIso.instFunLike piOrderIso Set.iInter Set Set.instHasSubset Set.preimage	—	Set.iInter_congr_Prop Set.image_congr
coe_piOrderIso_symm_apply 📖	mathematical	—	SetLike.coe Submodule Pi.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike DFunLike.coe RelIso Ideal Pi.hasLe Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder RelIso.instFunLike RelIso.symm piOrderIso setOf	—	—
coe_restrictScalars 📖	mathematical	—	SetLike.coe Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.setLike Submodule.restrictScalars Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ideal	—	—
comap_bot_le_of_injective 📖	mathematical	DFunLike.coe	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap Bot.bot Submodule.instBot	—	le_trans Submodule.zero_mem map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Submodule.mem_bot mem_comap bot_le
comap_bot_of_injective 📖	mathematical	DFunLike.coe	comap Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	le_bot_iff comap_bot_le_of_injective
comap_coe 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom RingHom.instRingHomClass	—	RingHom.instRingHomClass
comap_comap 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass RingHom.comp	—	RingHom.instRingHomClass
comap_comapₐ 📖	mathematical	—	comap AlgHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp	—	comap_comap
comap_eq_top_iff 📖	mathematical	—	comap Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	eq_top_iff_one mem_comap map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass comap_top
comap_finsetInf 📖	mathematical	—	comap Finset.inf Ideal Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instOrderTop	—	comap.congr_simp Finset.inf_eq_iInf comap_iInf
comap_iInf 📖	mathematical	—	comap iInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.u_iInf gc_map_comap
comap_id 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.id RingHom.instRingHomClass	—	ext RingHom.instRingHomClass
comap_idₐ 📖	mathematical	—	comap AlgHom AlgHom.funLike AlgHom.id AlgHomClass.toRingHomClass AlgHom.algHomClass	—	comap_id
comap_inf 📖	mathematical	—	comap Ideal Submodule.instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
comap_injective_of_surjective 📖	mathematical	DFunLike.coe	Ideal comap	—	GaloisInsertion.u_injective
comap_isMaximal_of_equiv 📖	mathematical	—	IsMaximal comap EquivLike.toFunLike RingEquivClass.toRingHomClass Semiring.toNonAssocSemiring	—	IsMaximal.comap_bijective RingEquivClass.toRingHomClass EquivLike.bijective
comap_isMaximal_of_surjective 📖	mathematical	DFunLike.coe	IsMaximal Ring.toSemiring comap	—	comap_ne_top IsMaximal.out lt_of_le_of_ne le_map_of_comap_le_of_surjective le_of_lt ne_of_lt trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv comap_map_of_surjective sup_eq_left le_trans comap_mono bot_le eq_top_iff comap_top sup_le le_of_eq
comap_isPrime 📖	mathematical	—	IsPrime comap	—	IsPrime.comap
comap_le_comap_iff_of_surjective 📖	mathematical	DFunLike.coe	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	—	LE.le.trans Eq.le map_comap_of_surjective map_le_of_le_comap le_comap_of_map_le
comap_le_iff_le_map 📖	mathematical	Function.Bijective DFunLike.coe	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap map	—	le_map_of_comap_le_of_surjective comap_mono Equiv.right_inv
comap_le_map_of_inv_on 📖	mathematical	Set.LeftInvOn DFunLike.coe Set.preimage SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder comap map	—	mem_map_of_mem
comap_le_map_of_inverse 📖	mathematical	DFunLike.coe	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap map	—	comap_le_map_of_inv_on Function.LeftInverse.leftInvOn
comap_map_comap 📖	mathematical	—	comap map	—	GaloisConnection.u_l_u_eq_u gc_map_comap
comap_map_eq_self_iff_of_isPrime 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass map IsPrime	—	RingHom.instRingHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass exists_le_prime_disjoint disjoint_map_primeCompl_iff_comap_le Eq.le le_antisymm map_le_iff_le_comap comap_map_comap
comap_map_eq_self_of_isMaximal 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass map	—	RingHom.instRingHomClass IsCoatom.le_iff_eq IsMaximal.out comap_ne_top le_comap_map
comap_map_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe	comap map	—	le_antisymm comap_le_iff_le_map le_comap_map
comap_map_of_surjective 📖	mathematical	DFunLike.coe	comap Ring.toSemiring map Ideal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Submodule.instBot	—	le_antisymm mem_image_of_mem_map_of_surjective Submodule.mem_sup Submodule.mem_bot map_sub RingHomClass.toAddMonoidHomClass sub_self add_sub_cancel sup_le map_le_iff_le_comap le_rfl comap_mono bot_le
comap_map_of_surjective' 📖	mathematical	DFunLike.coe	comap Ring.toSemiring map Ideal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker	—	comap_map_of_surjective
comap_mono 📖	mathematical	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	comap	—	Set.preimage_mono
comap_ne_top 📖	—	—	—	—	ne_top_iff_one mem_comap map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
comap_of_equiv 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.instRingHomClass RingEquiv.symm	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.instRingHomClass RingEquiv.toRingHom_eq_coe comap_comap RingEquiv.symm_comp comap_id
comap_radical 📖	mathematical	—	comap CommSemiring.toSemiring radical	—	ext map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
comap_sInf 📖	mathematical	—	comap InfSet.sInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iInf Set Set.instMembership	—	GaloisConnection.u_sInf gc_map_comap
comap_sInf' 📖	mathematical	—	comap InfSet.sInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iInf Set Set.instMembership Set.image	—	trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv comap_sInf iInf_image
comap_symm 📖	mathematical	—	comap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_comap_of_equiv
comap_top 📖	mathematical	—	comap Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.u_top gc_map_comap
disjoint_map_primeCompl_iff_comap_le 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike Submonoid.map CommSemiring.toSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass primeCompl Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder comap	—	RingHom.instRingHomClass Set.disjoint_image_right disjoint_compl_right_iff
exists_ideal_comap_le_prime 📖	mathematical	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap CommSemiring.toSemiring	IsPrime	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass exists_le_prime_disjoint Set.disjoint_left of_not_not
gc_map_comap 📖	mathematical	—	GaloisConnection Ideal PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map comap	—	map_le_iff_le_comap
instIsPrincipalIdealRingForallOfFinite 📖	mathematical	IsPrincipalIdealRing	Pi.semiring	—	OrderIso.symm_apply_apply IsPrincipalIdealRing.principal Submodule.IsPrincipal.span_singleton_generator pi_span
instIsTwoSidedComap 📖	mathematical	—	IsTwoSided comap	—	mem_comap map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_mem_right
instIsTwoSidedMapRingHomOfRingHomSurjective 📖	mathematical	—	IsTwoSided map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	map_eq_submodule_map RingHom.surjective RingHom.coe_toSemilinearMap map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_mem_right
isMaximal_comap_iff_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe	IsMaximal comap	—	OrderIso.isCoatom_iff
isMaximal_iff_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe	IsMaximal Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsMaximal.map_bijective map_bot RingHomClass.toNonUnitalRingHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.bijective
isMaximal_map_iff_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe	IsMaximal map	—	OrderIso.isCoatom_iff
ker_le_comap 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker comap	—	mem_comap zero_mem RingHom.mem_ker
le_comap_map 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap map	—	GaloisConnection.le_u_l gc_map_comap
le_comap_mul 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.mul IsScalarTower.right Algebra.id comap	—	IsScalarTower.right map_le_iff_le_comap mul_mono le_rfl IsScalarTower.left map_mul
le_comap_of_map_le 📖	mathematical	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map	comap	—	GaloisConnection.le_u gc_map_comap
le_comap_pow 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id comap	—	IsScalarTower.right pow_zero one_eq_top Eq.le pow_succ LE.le.trans IsScalarTower.left mul_mono_left le_comap_mul
le_comap_sup 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice comap	—	Monotone.le_map_sup GaloisConnection.monotone_u gc_map_comap
le_map_of_comap_le_of_surjective 📖	mathematical	DFunLike.coe Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	map	—	map_mono map_comap_of_surjective
mapHom_apply 📖	mathematical	—	DFunLike.coe RingHom Ideal CommSemiring.toSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id RingHom.instFunLike mapHom map	—	—
map_bot 📖	mathematical	—	map Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.l_bot gc_map_comap
map_coe 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom	—	—
map_comap_eq_self_of_equiv 📖	mathematical	—	map EquivLike.toFunLike comap RingEquivClass.toRingHomClass Semiring.toNonAssocSemiring	—	map_comap_of_surjective RingEquivClass.toRingHomClass EquivLike.surjective
map_comap_le 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map comap	—	GaloisConnection.l_u_le gc_map_comap
map_comap_map 📖	mathematical	—	map comap	—	GaloisConnection.l_u_l_eq_l gc_map_comap
map_comap_of_equiv 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass comap RingEquiv.symm	—	le_antisymm RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_le_comap_of_inverse Equiv.left_inv' comap_le_map_of_inverse Equiv.right_inv'
map_comap_of_surjective 📖	mathematical	DFunLike.coe	map comap	—	le_antisymm map_le_iff_le_comap le_rfl mem_map_of_mem
map_eq_bot_iff_le_ker 📖	mathematical	—	map Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder RingHom.ker	—	RingHom.ker.eq_1 eq_bot_iff map_le_iff_le_comap
map_eq_bot_iff_of_injective 📖	mathematical	DFunLike.coe	map Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Submodule.eq_bot_iff
map_eq_iff_sup_ker_eq_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	map Ideal SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id RingHom.ker RingHom.instRingHomClass	—	RingHom.instRingHomClass comap_injective_of_surjective comap_map_of_surjective RingHom.ker_eq_comap_bot
map_eq_submodule_map 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submodule.map NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.toSemilinearMap	—	Submodule.ext mem_map_iff_of_surjective RingHom.instRingHomClass RingHomSurjective.is_surjective
map_eq_top_or_isMaximal_of_surjective 📖	mathematical	DFunLike.coe	map Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsMaximal	—	comap_injective_of_surjective IsMaximal.out LE.le.trans_lt le_comap_map OrderEmbedding.strictMono
map_evalRingHom_pi 📖	mathematical	—	map RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring Pi.semiring RingHom.instFunLike Pi.evalRingHom pi	—	ext mem_map_iff_of_surjective RingHom.instRingHomClass Function.surjective_eval Zero.instNonempty single_mem_pi Pi.single_eq_same
map_iInf_comap_of_surjective 📖	mathematical	DFunLike.coe	map iInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	—	GaloisInsertion.l_iInf_u
map_iSup 📖	mathematical	—	map iSup Ideal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.l_iSup gc_map_comap
map_iSup_comap_of_surjective 📖	mathematical	DFunLike.coe	map iSup Ideal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	—	GaloisInsertion.l_iSup_u
map_id 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.id	—	GaloisConnection.l_unique RingHom.instRingHomClass gc_map_comap GaloisConnection.id comap_id
map_idₐ 📖	mathematical	—	map AlgHom AlgHom.funLike AlgHom.id	—	map_id
map_inf_comap_of_surjective 📖	mathematical	DFunLike.coe	map Ideal Submodule.instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	—	GaloisInsertion.l_inf_u
map_inf_le 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map Submodule.instMin	—	Monotone.map_inf_le GaloisConnection.monotone_l gc_map_comap
map_isMaximal_of_equiv 📖	mathematical	—	IsMaximal map EquivLike.toFunLike	—	IsMaximal.map_bijective RingEquivClass.toRingHomClass EquivLike.bijective
map_isPrime_of_equiv 📖	mathematical	—	IsPrime map EquivLike.toFunLike	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_comap_of_equiv IsPrime.comap
map_isPrime_of_surjective 📖	mathematical	DFunLike.coe Ideal Ring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker	IsPrime map	—	IsPrime.ne_top eq_top_iff sup_le le_of_eq comap_top comap_map_of_surjective mem_map_iff_of_surjective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add zero_add Mathlib.Tactic.Abel.zero_termg sub_mem map_sub RingHomClass.toAddMonoidHomClass sub_eq_zero mem_map_of_mem IsPrime.mem_or_mem
map_le_comap_of_inv_on 📖	mathematical	Set.LeftInvOn DFunLike.coe SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder map comap	—	span_le SetLike.mem_coe mem_comap
map_le_comap_of_inverse 📖	mathematical	DFunLike.coe	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map comap	—	map_le_comap_of_inv_on Function.LeftInverse.leftInvOn
map_le_iff_le_comap 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map comap	—	span_le Set.image_subset_iff
map_le_of_le_comap 📖	mathematical	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	map	—	GaloisConnection.l_le gc_map_comap
map_map 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.comp	—	GaloisConnection.l_unique RingHom.instRingHomClass GaloisConnection.compose gc_map_comap comap_comap
map_mapₐ 📖	mathematical	—	map AlgHom AlgHom.funLike AlgHom.comp	—	map_map
map_mono 📖	mathematical	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	map	—	span_mono Set.image_mono
map_mul 📖	mathematical	—	map CommSemiring.toSemiring Ideal Submodule.mul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction IsScalarTower.right Algebra.id	—	le_antisymm IsScalarTower.left IsScalarTower.right map_le_iff_le_comap mul_le map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_mem_mul mem_map_of_mem span_le span_mul_span instIsTwoSided
map_ne_bot_of_ne_bot 📖	—	—	—	—	Function.mt map_eq_bot_iff_of_injective RingHom.instRingHomClass FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero
map_of_equiv 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.toRingHom_eq_coe map_map RingEquiv.symm_comp map_id
map_pointwise_smul 📖	mathematical	—	map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id DFunLike.coe	—	Algebra.to_smulCommClass IsScalarTower.left smulCommClass_self Submodule.ideal_span_singleton_smul IsScalarTower.right smul_eq_mul map_mul RingHom.instRingHomClass map_span Set.image_singleton
map_pow 📖	mathematical	—	map CommSemiring.toSemiring Ideal Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_radical_le 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map radical	—	map_le_iff_le_comap mem_map_of_mem map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
map_radical_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.ker RingHom.instRingHomClass	map radical	—	RingHom.instRingHomClass radical_eq_sInf LE.le.trans map_le_iff_le_comap comap_isPrime map_comap_of_surjective map_mono map_isPrime_of_surjective le_trans map_sInf
map_sInf 📖	mathematical	DFunLike.coe Ideal Ring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker	map InfSet.sInf Submodule.instInfSet Set.image	—	le_antisymm le_sInf mem_map_iff_of_surjective Set.mem_image mem_map_of_mem sInf_le_of_le le_of_eq Submodule.mem_sInf RingHom.mem_ker map_sub RingHomClass.toAddMonoidHomClass sub_self sub_add_cancel Submodule.add_mem
map_sSup 📖	mathematical	—	map SupSet.sSup Ideal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iSup Set Set.instMembership	—	GaloisConnection.l_sSup gc_map_comap
map_span 📖	mathematical	—	map span Set.image DFunLike.coe	—	Submodule.span_eq_of_le mem_map_of_mem subset_span map_le_iff_le_comap span_le coe_comap Set.image_subset_iff
map_sup 📖	mathematical	—	map Ideal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.l_sup gc_map_comap
map_sup_comap_of_surjective 📖	mathematical	DFunLike.coe	map Ideal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap	—	GaloisInsertion.l_sup_u
map_surjective_of_surjective 📖	mathematical	DFunLike.coe	Ideal map	—	GaloisInsertion.l_surjective
map_symm 📖	mathematical	—	map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm comap RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	—	map_comap_of_equiv
map_top 📖	mathematical	—	map Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	eq_top_iff_one subset_span map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
mem_comap 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap DFunLike.coe	—	—
mem_image_of_mem_map_of_surjective 📖	mathematical	DFunLike.coe Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map	Set Set.instMembership Set.image SetLike.coe	—	Submodule.span_induction zero_mem map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass add_mem map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass mul_mem_left map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
mem_map_iff_of_surjective 📖	mathematical	DFunLike.coe	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map	—	Set.mem_image mem_image_of_mem_map_of_surjective mem_map_of_mem
mem_map_of_equiv 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map EquivLike.toFunLike DFunLike.coe	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_comap_of_equiv RingEquiv.apply_symm_apply mem_map_of_mem
mem_map_of_mem 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	map DFunLike.coe	—	subset_span
ne_bot_of_map_ne_bot 📖	—	—	—	—	map_bot
restrictScalars_mul 📖	mathematical	—	Submodule.restrictScalars NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ideal Submodule.mul IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Submodule	—	IsScalarTower.left
smul_restrictScalars 📖	mathematical	—	Submodule.restrictScalars CommSemiring.toSemiring Algebra.toSMul Ideal Submodule Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsScalarTower.left Submodule.restrictScalars.congr_simp Submodule.span_smul_eq smulCommClass_self Submodule.set_smul_eq_iSup iSup_congr_Prop iSup_image map_iSup₂ FrameHomClass.tosSupHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass
smul_top_eq_map 📖	mathematical	—	Ideal CommSemiring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop Submodule.restrictScalars Algebra.toSMul IsScalarTower.right map RingHom RingHom.instFunLike algebraMap	—	IsScalarTower.left IsScalarTower.right smul_restrictScalars smul_eq_mul mul_top instIsTwoSided
symm_apply_mem_of_equiv_iff 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm map	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass comap_symm mem_comap

Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_bijective 📖	mathematical	Function.Bijective DFunLike.coe	Ideal.IsMaximal Ideal.comap	—	Ideal.isMaximal_comap_iff_of_bijective
comap_piEvalRingHom 📖	mathematical	—	Ideal.IsMaximal Pi.semiring Ideal.comap RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring RingHom.instFunLike Pi.evalRingHom RingHom.instRingHomClass	—	RingHom.instRingHomClass Ideal.isMaximal_iff Ideal.ne_top_iff_one ne_top exists_inv eq_or_ne Function.update_self Function.update_of_ne MulZeroClass.zero_mul zero_add Ideal.add_mem Ideal.mul_mem_left
map_bijective 📖	mathematical	Function.Bijective DFunLike.coe	Ideal.IsMaximal Ideal.map	—	Ideal.isMaximal_map_iff_of_bijective
map_of_surjective_of_ker_le 📖	mathematical	DFunLike.coe Ideal Ring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker	Ideal.IsMaximal Ideal.map	—	Ideal.map_eq_top_or_isMaximal_of_surjective ne_top sup_of_le_left RingHom.ker_eq_comap_bot Ideal.comap_top Ideal.comap_map_of_surjective

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	—	Ideal.IsPrime Ideal.comap	—	Ideal.comap_ne_top ne_top' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mem_or_mem'

Ideal.IsRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Ideal.IsRadical	Ideal.comap CommSemiring.toSemiring	—	radical Ideal.comap_radical Ideal.radical_isRadical

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_eq 📖	mathematical	—	Module.annihilator	—	RingHomInvPair.ids LE.le.antisymm LinearMap.annihilator_le_of_surjective surjective LinearMap.annihilator_le_of_injective injective

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_le_of_injective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Module.annihilator	—	Module.mem_annihilator map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass map_zero
annihilator_le_of_surjective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Module.annihilator	—	Module.mem_annihilator map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass map_zero

Module

Definitions

Name	Category	Theorems
annihilator 📖	CompOp	31 math math: mem_annihilator, Submodule.annihilator_quotient, supportDim_eq_ringKrullDim_quotient_annihilator, mem_support_iff_of_finite, IsSemisimpleModule.jacobson_le_annihilator, isTorsionBySet_annihilator, IsSemisimpleModule.annihilator_isRadical, comap_annihilator, LinearMap.annihilator_le_of_injective, annihilator_eq_top_iff, instIsTwoSidedAnnihilator, Ideal.annihilator_quotient, annihilator_eq_bot, Polynomial.span_minpoly_eq_annihilator, annihilator_pi, associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes, Submodule.annihilator_top, support_eq_zeroLocus, IsSMulRegular.subsingleton_linearMap_iff, annihilator_dfinsupp, isTorsionBySet_iff_subset_annihilator, Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors, annihilator_finsupp, LinearMap.annihilator_le_of_surjective, exists_ker_toSpanSingleton_eq_annihilator, IsSimpleModule.annihilator_isMaximal, LinearEquiv.annihilator_eq, isTorsionBy_iff_mem_annihilator, AEval.annihilator_eq_ker_aeval, annihilator_le_of_mem_support, annihilator_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_dfinsupp 📖	mathematical	—	annihilator DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module iInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext DFinsupp.single_apply DFunLike.congr_fun DFinsupp.ext
annihilator_eq_bot 📖	mathematical	—	annihilator Ring.toSemiring AddCommGroup.toAddCommMonoid Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule FaithfulSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction	—	le_bot_iff sub_eq_zero mem_annihilator sub_smul sub_self zero_smul
annihilator_eq_top_iff 📖	mathematical	—	annihilator Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	one_smul mem_annihilator Submodule.mem_top top_le_iff
annihilator_finsupp 📖	mathematical	—	annihilator Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module	—	Ideal.ext Finsupp.smul_single Finsupp.single_eq_same Finsupp.ext
annihilator_pi 📖	mathematical	—	annihilator Pi.addCommMonoid Pi.module iInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext Pi.single_eq_same
annihilator_prod 📖	mathematical	—	annihilator Prod.instAddCommMonoid Prod.instModule Ideal Submodule.instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext Zero.instNonempty
comap_annihilator 📖	mathematical	—	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass annihilator	—	Ideal.ext RingHom.instRingHomClass algebraMap_smul
mem_annihilator 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction	—	AddMonoidHom.ext

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_ringHom 📖	mathematical	—	RingHom.ker RingHom Semiring.toNonAssocSemiring nonAssocSemiring semiring RingHom.instFunLike RingHom.instRingHomClass ringHom iInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Ideal.ext RingHom.instRingHomClass

RingEquiv

Definitions

Name	Category	Theorems
idealComapOrderIso 📖	CompOp	2 math math: idealComapOrderIso_apply, idealComapOrderIso_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealComapOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RelIso.instFunLike idealComapOrderIso Ideal.comap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike	—	—
idealComapOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instFunLikeOrderIso OrderIso.symm idealComapOrderIso Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike	—	—

RingHom

Definitions

Name	Category	Theorems
ker 📖	CompOp	164 math math: Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt, KaehlerDifferential.kerCotangentToTensor_toCotangent, PrimeSpectrum.closure_range_comap, Polynomial.ker_mapRingHom, ker_evalRingHom, Polynomial.ker_evalRingHom, IsAdjoinRoot.mem_ker_map, smoothSheafCommRing.nonunits_stalk, AlgHom.ker_coe, IsLocalRing.ker_residue, algebraicIndependent_iff_ker_eq_bot, ker_eq_top_of_subsingleton, MvPolynomial.ker_map, Ideal.ker_algebraMap_residueField, Polynomial.fiberEquivQuotient_tmul, range_comap_of_surjective, quotientKerEquivOfSurjective_symm_apply, KaehlerDifferential.cotangentComplexBaseChange_tmul, PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical, liftOfSurjective_comp, TruncatedWittVector.iInf_ker_truncate, AlgebraicIndependent.repr_ker, range_specComap_of_surjective, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, KaehlerDifferential.kerToTensor_apply, ker_equiv, liftOfSurjective_comp_apply, PrimeSpectrum.vanishingIdeal_range_comap, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, ker_rangeRestrict, quotientKerEquivOfSurjective_symm_comp, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, ker_isMaximal_of_surjective, Algebra.Generators.map_toComp_ker, Ideal.ker_Pi_Quotient_mk, comap_ker, CharP.ker_intAlgebraMap_eq_span, ker_isRadical_iff_reduced_of_surjective, Ideal.kerLiftAlg_injective, Pi.ker_ringHom, Algebra.TensorProduct.map_ker, mem_ker, KaehlerDifferential.End_equiv_aux, AlgebraicGeometry.Scheme.ker_of_isAffine, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, AlgHom.comap_ker, Algebra.FinitePresentation.ker_fg_of_mvPolynomial, Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, smoothSheafCommRing.isUnit_stalk_iff, Polynomial.ker_constantCoeff, AlgHom.ker_rangeRestrict, Module.support_of_algebra, Ideal.quotientKerAlgEquivOfRightInverse_symm_apply, AlgHom.ker_coe_equiv, NumberField.RingOfIntegers.ker_algebraMap_eq_bot, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, AlgHom.toKerIsLocalization_apply, Algebra.FormallySmooth.iff_of_surjective, IsLocalRing.ker_eq_maximalIdeal, AlgebraicGeometry.Scheme.Hom.ker_apply, Ideal.quotientKerAlgEquivOfRightInverse_apply, IsPerfectClosure.ker_eq, AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective, DoubleQuot.ker_quotQuotMk, WittVector.mem_ker_truncate, toKerIsLocalization_apply, minpoly.ker_aeval_eq_span_minpoly, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AdicCompletion.kerProj_surjective, ContinuousMap.AlgHom.closure_ker_inter, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Algebra.FinitePresentation.ker_fG_of_surjective, instIsTwoSidedKer, WittVector.ker_map_le_ker_mk_comp_ghostComponent, Ideal.kerLiftAlg_toRingHom, tensorKaehlerQuotKerSqEquiv_tmul_D, ker_eq_bot_iff_eq_zero, Ideal.quotientKerAlgEquivOfSurjective_apply, liftOfRightInverse_comp_apply, quotientKerEquivOfRightInverse.Symm.apply, transcendental_iff_ker_eq_bot, Ideal.Quotient.mkₐ_ker, Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective, quotientKerEquivOfSurjective_apply_mk, PrimeSpectrum.range_comap_snd, Ideal.injective_lift_iff, Ideal.ker_le_comap, IsPRadical.ker_le, Ideal.Quotient.factor_ker, DoubleQuot.ker_quotLeftToQuotSup, ker_coe_toRingHom, ker_comp_of_injective, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, Ideal.minimalPrimes_map_of_surjective, one_notMem_ker, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, pNilradical_le_ker_of_perfectRing, PadicInt.ker_toZModPow, AdicCompletion.kerProj_of, DividedPowers.isSubDPIdeal_ker, kerLift_injective, Algebra.FormallySmooth.iff_split_surjection, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, liftOfRightInverse_comp, injective_iff_ker_eq_bot, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, MvPolynomial.ker_mapAlgHom, WeakDual.ker_isMaximal, ZMod.ker_intCastRingHom, ker_eq_comap_bot, ker_isPrime, IsLocalization.ker_map, Ideal.quotientKerAlgEquivOfSurjective_symm_apply, Ideal.quotientKerAlgEquivOfSurjective_mk, Ideal.map_eq_iff_sup_ker_eq_of_surjective, Ideal.ker_quotientMap_mk, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, Algebra.TensorProduct.lTensor_ker, PowerSeries.ker_coeff_eq_max_ideal, ker_coe_equiv, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Generators.ker_ofAlgHom, AlgHom.ker_kerSquareLift, Module.AEval.annihilator_top_eq_ker_aeval, quotientKerEquivOfRightInverse.apply, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, Ideal.KerLift.map_smul, PadicInt.ker_toZMod, Algebra.FinitePresentation.out, FaithfulSMul.ker_algebraMap_eq_bot, ker_equiv_comp, AlgHom.toKerIsLocalization_isLocalizedModule, Ideal.comap_map_of_surjective', WittVector.ker_constantCoeff, Ideal.mk_ker, KaehlerDifferential.range_kerCotangentToTensor, sub_mem_ker_iff, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, CharP.quotient_iff_le_ker_natCast, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, isPRadical_iff, ker_eq, AlgebraicGeometry.Scheme.Hom.toImage_app, Algebra.FormallyEtale.iff_of_surjective, PrimeSpectrum.range_comap_fst, AlgHom.kerSquareLift_mk, IsPRadical.ker_le', Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, kerLift_mk, minpoly.ker_eval, toKerIsLocalization_isLocalizedModule, Module.AEval.annihilator_eq_ker_aeval, Algebra.TensorProduct.rTensor_ker, HomogeneousIdeal.toIdeal_irrelevant, IsAdjoinRoot.ker_map, Algebra.FormallySmooth.iff_split_injection, Ideal.kerLiftAlg_mk, Ideal.map_eq_bot_iff_le_ker, derivationQuotKerSq_mk, ker_rangeSRestrict, Algebra.FinitePresentation.iff_quotient_mvPolynomial'
liftOfRightInverse 📖	CompOp	3 math math: eq_liftOfRightInverse, liftOfRightInverse_comp_apply, liftOfRightInverse_comp
liftOfRightInverseAux 📖	CompOp	1 math math: liftOfRightInverseAux_comp_apply
liftOfSurjective 📖	CompOp	3 math math: liftOfSurjective_comp, liftOfSurjective_comp_apply, eq_liftOfSurjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_ker 📖	mathematical	—	Ideal.comap RingHom Semiring.toNonAssocSemiring instFunLike instRingHomClass ker comp	—	instRingHomClass ker_eq_comap_bot Ideal.comap_comap
eq_liftOfRightInverse 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass comp	Equiv EquivLike.toFunLike Equiv.instEquivLike liftOfRightInverse	—	instRingHomClass Equiv.apply_symm_apply
eq_liftOfSurjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass comp	Equiv EquivLike.toFunLike Equiv.instEquivLike liftOfSurjective	—	instRingHomClass eq_liftOfRightInverse
injective_iff_ker_eq_bot 📖	mathematical	—	DFunLike.coe ker Ring.toSemiring Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	SetLike.ext'_iff ker_eq Set.ext_iff injective_iff_map_eq_zero' RingHomClass.toAddMonoidHomClass
instIsTwoSidedKer 📖	mathematical	—	Ideal.IsTwoSided ker	—	Ideal.instIsTwoSidedComap Ideal.instIsTwoSidedBot
ker_coe_equiv 📖	mathematical	—	ker RingHom Semiring.toNonAssocSemiring instFunLike instRingHomClass RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule	—	Ideal.ext instRingHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass
ker_coe_toRingHom 📖	mathematical	—	ker RingHom Semiring.toNonAssocSemiring instFunLike instRingHomClass RingHomClass.toRingHom	—	instRingHomClass
ker_comp_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike	ker instRingHomClass comp	—	instRingHomClass comap_ker injective_iff_ker_eq_bot ker.eq_1
ker_eq 📖	mathematical	—	SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker Set.preimage DFunLike.coe Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
ker_eq_bot_iff_eq_zero 📖	mathematical	—	ker Ring.toSemiring Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass injective_iff_ker_eq_bot
ker_eq_comap_bot 📖	mathematical	—	ker Ideal.comap Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
ker_eq_top_of_subsingleton 📖	mathematical	—	ker Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	eq_top_iff
ker_equiv 📖	mathematical	—	ker EquivLike.toFunLike RingEquivClass.toRingHomClass Semiring.toNonAssocSemiring Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Ideal.ext RingEquivClass.toRingHomClass EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass
ker_equiv_comp 📖	mathematical	—	ker RingHom Semiring.toNonAssocSemiring instFunLike instRingHomClass comp RingEquiv.toRingHom	—	instRingHomClass comap_ker RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.toRingHom_eq_coe ker_coe_equiv ker.eq_1
ker_evalRingHom 📖	mathematical	—	ker RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Pi.semiring instFunLike instRingHomClass Pi.evalRingHom Ideal.span Set Set.instSingletonSet Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	le_antisymm instRingHomClass Ideal.mem_span_singleton mul_add Distrib.leftDistribClass sub_mul one_mul MulZeroClass.mul_zero Pi.single_zero sub_zero Pi.single_eq_same mul_one sub_self add_zero
ker_isMaximal_of_surjective 📖	mathematical	DFunLike.coe	Ideal.IsMaximal Ring.toSemiring ker DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	—	Ideal.bot_isMaximal Ideal.comap_isMaximal_of_surjective
ker_isPrime 📖	mathematical	—	Ideal.IsPrime ker	—	Ideal.IsPrime.comap Ideal.isPrime_bot IsDomain.toNontrivial IsDomain.to_noZeroDivisors
ker_ne_top 📖	—	—	—	—	Ideal.ne_top_iff_one one_notMem_ker
ker_rangeRestrict 📖	mathematical	—	ker Subring SetLike.instMembership Subring.instSetLike range RingHom Semiring.toNonAssocSemiring Ring.toSemiring Subring.toRing instFunLike instRingHomClass rangeRestrict	—	Ideal.ext instRingHomClass
ker_rangeSRestrict 📖	mathematical	—	ker Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership Subsemiring.instSetLike rangeS RingHom Subsemiring.toNonAssocSemiring Subsemiring.toSemiring instFunLike instRingHomClass rangeSRestrict	—	Ideal.ext instRingHomClass
liftOfRightInverseAux_comp_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass	liftOfRightInverseAux	—	instRingHomClass AddMonoidHom.liftOfRightInverse_comp_apply
liftOfRightInverse_comp 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike	comp Equiv Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass EquivLike.toFunLike Equiv.instEquivLike liftOfRightInverse	—	instRingHomClass ext liftOfRightInverse_comp_apply
liftOfRightInverse_comp_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike	Equiv Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass EquivLike.toFunLike Equiv.instEquivLike liftOfRightInverse	—	instRingHomClass liftOfRightInverseAux_comp_apply
liftOfSurjective_comp 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike	comp Equiv Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass EquivLike.toFunLike Equiv.instEquivLike liftOfSurjective	—	instRingHomClass liftOfRightInverse_comp
liftOfSurjective_comp_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring instFunLike	Equiv Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker instRingHomClass EquivLike.toFunLike Equiv.instEquivLike liftOfSurjective	—	instRingHomClass liftOfRightInverse_comp_apply
mem_ker 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker DFunLike.coe MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ker.eq_1 Ideal.mem_comap Submodule.mem_bot
one_notMem_ker 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_ker map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass one_ne_zero NeZero.one
sub_mem_ker_iff 📖	mathematical	—	Ideal Ring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ker SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe	—	mem_ker map_sub RingHomClass.toAddMonoidHomClass sub_eq_zero

Submodule

Definitions

Name	Category	Theorems
annihilator 📖	CompOp	28 math math: le_annihilator_iff, isInternal_prime_power_torsion_of_pid, mul_annihilator, annihilator_iSup, annihilator_mul, mem_annihilator', mem_annihilator, annihilator_smul, annihilator_map_mkQ_eq_colon, annihilator_bot, Module.mem_support_iff_exists_annihilator, annihilator_top_inter_nonZeroDivisors, annihilator_span_singleton, annihilator_mono, bot_colon', Module.isTorsionBySet_annihilator_top, annihilator_span, mem_annihilator_span, torsion_gc, IsAssociatedPrime.annihilator_le, isInternal_prime_power_torsion, annihilator_top, Module.AEval.annihilator_top_eq_ker_aeval, coe_torsion_eq_annihilator_ne_bot, mem_annihilator_span_singleton, Module.mem_support_iff_of_span_eq_top, bot_colon, annihilator_eq_top_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_bot 📖	mathematical	—	annihilator Bot.bot Submodule instBot Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	top_le_iff mem_annihilator smul_zero
annihilator_eq_top_iff 📖	mathematical	—	annihilator Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Submodule instBot	—	annihilator.eq_1 Module.annihilator_eq_top_iff subsingleton_iff_eq_bot
annihilator_iSup 📖	mathematical	—	annihilator iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice iInf Ideal instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	le_antisymm le_iInf annihilator_mono le_iSup mem_annihilator iSup_induction mem_iInf smul_zero smul_add add_zero
annihilator_mono 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder	Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator	—	mem_annihilator
annihilator_mul 📖	mathematical	—	Ideal mul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction annihilator Bot.bot instBot	—	annihilator_smul
annihilator_smul 📖	mathematical	—	Ideal Submodule instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction annihilator Bot.bot instBot	—	IsScalarTower.left eq_bot_iff smul_le mem_annihilator
annihilator_span 📖	mathematical	—	annihilator CommSemiring.toSemiring span iInf Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set.Elem instInfSet LinearMap.ker RingHom.id LinearMap.toSpanSingleton Set Set.instMembership	—	Ideal.ext
annihilator_span_singleton 📖	mathematical	—	annihilator CommSemiring.toSemiring span Set Set.instSingletonSet LinearMap.ker NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.toSpanSingleton	—	annihilator_span ciInf_unique
annihilator_top 📖	mathematical	—	annihilator Top.top Submodule instTop Module.annihilator	—	LinearEquiv.annihilator_eq
le_annihilator_iff 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator Submodule instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Bot.bot instBot	—	IsScalarTower.left instIsConcreteLE
mem_annihilator 📖	mathematical	—	Ideal SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
mem_annihilator' 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder comap RingHom.id LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.id Bot.bot instBot	—	smulCommClass_self mem_annihilator mem_bot
mem_annihilator_span 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator span SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership	—	mem_annihilator subset_span Subtype.prop span_induction smul_zero smul_add zero_add SMulCommClass.smul_comm smulCommClass_self
mem_annihilator_span_singleton 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annihilator span Set Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
mul_annihilator 📖	mathematical	—	Ideal CommSemiring.toSemiring mul Semiring.toModule IsScalarTower.right Algebra.id annihilator NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Bot.bot instBot	—	IsScalarTower.right mul_comm IsScalarTower.left annihilator_mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
element_smul_restrictScalars 📖	mathematical	—	Submodule.restrictScalars CommSemiring.toSemiring Algebra.toSMul Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	SetLike.coe_injective smulCommClass_self algebraMap_smul
instIsPrincipalMapRingHom 📖	mathematical	—	Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike	—	Submodule.IsPrincipal.principal Ideal.span.eq_1 Set.image_singleton Ideal.map_span RingHom.instRingHomClass Ideal.submodule_span_eq
instIsTwoSidedAnnihilator 📖	mathematical	—	Ideal.IsTwoSided Module.annihilator	—	RingHom.instIsTwoSidedKer

---

← Back to Index