Over

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

Statistics

Metric	Count
Definitions `LiesOver`, `algEquivOfEqComap`, `algEquivOfEqMap`, `algebraOfLiesOver`, `algebraQuotientMapQuotient`, `stabilizerHom`, `primesOver`, `mk`, `under`	9
Theorems `under`, `of_eq_comap`, `of_eq_map_equiv`, `over`, `smul`, `tower_bot`, `trans`, `algEquivOfEqComap_apply`, `algEquivOfEqMap_apply`, `algebraMap_mk_of_liesOver`, `algebraMap_quotient_map_quotient`, `instFaithfulSMul`, `instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver`, `isScalarTower_of_liesOver`, `ker_stabilizerHom`, `map_ker_stabilizer_subtype`, `mk_smul_mk_quotient_map_quotient`, `nontrivial_of_liesOver_of_isPrime`, `nontrivial_of_liesOver_of_ne_top`, `stabilizerHom_apply`, `tower_quotient_map_quotient`, `bot_liesOver_bot`, `comap_eq_of_scalar_tower_quotient`, `comap_liesOver`, `disjoint_primeCompl_of_liesOver`, `eq_top_iff_of_liesOver`, `instLiesOverBotOfIsPrime`, `liesOver_iff`, `map_equiv_liesOver`, `map_under_le_under_map`, `mem_of_liesOver`, `ne_bot_of_liesOver_of_ne_bot`, `ne_bot_of_mem_primesOver`, `ne_top_iff_of_liesOver`, `over_def`, `over_under`, `isPrime`, `liesOver`, `top_liesOver_top`, `under_bot`, `under_def`, `under_liesOver_of_liesOver`, `under_map_eq_map_under`, `under_smul`, `under_top`, `under_under`	46
Total	55

Ideal

Definitions

Name	Category	Theorems
`LiesOver` 📖	CompData	35 math math: `IsLocalization.AtPrime.liesOver_map_of_liesOver`, `LiesOver.of_eq_comap`, `instLiesOverFiberOfIsPrime`, `LiesOver.smul`, `liesOver_iff_dvd_map`, `Localization.localRingHom_injective_of_primesOver_eq_singleton`, `exists_maximal_ideal_liesOver_of_isIntegral`, `IsLocalRing.ResidueField.instLiesOverMaximalIdeal`, `LiesOver.of_eq_map_equiv`, `exists_ideal_le_liesOver_of_le`, `liesOver_iff`, `exists_ideal_liesOver_maximal_of_isIntegral`, `IsLocalization.AtPrime.liesOver_comap_of_liesOver`, `NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm`, `exists_ideal_lt_liesOver_of_lt`, `IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one`, `comap_liesOver`, `top_liesOver_top`, `instLiesOverResidueFieldBotIdeal`, `primesOver.liesOver`, `Factors.liesOver`, `exists_isPrime_liesOver_of_faithfullyFlat`, `over_under`, `instLiesOverBotOfIsPrime`, `LiesOver.trans`, `PrimeSpectrum.instLiesOverAsIdealComapAlgebraMap`, `map_equiv_liesOver`, `Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt`, `under_liesOver_of_liesOver`, `IsLocalization.AtPrime.liesOver_maximalIdeal`, `Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal`, `bot_liesOver_bot`, `Int.liesOver_span_absNorm`, `LiesOver.tower_bot`, `IsLocalization.liesOver_of_isPrime_of_disjoint`
`primesOver` 📖	CompOp	43 math math: `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective`, `comap_fiberIsoOfBijectiveResidueField_apply`, `IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow`, `coe_smul_primesOver_mk_eq_map_galRestrict`, `ncard_primesOver_mul_ncard_primesOver`, `coe_primesOverFinset`, `one_le_primesOver_ncard`, `IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq`, `primesOver_bot`, `Algebra.QuasiFinite.iff_finite_primesOver`, `IsDedekindDomain.primesOverEquivPrimesOver_apply`, `Algebra.IsInvariant.orbit_eq_primesOver`, `ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn`, `IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq`, `primesOver_finite`, `nonempty_primesOver`, `isPretransitive_of_isGalois`, `coe_smul_primesOver_mk`, `IsCyclotomicExtension.Rat.ncard_primesOver_of_prime`, `isPretransitive_of_isGaloisGroup`, `mem_primesOverFinset_iff`, `primesOver.liesOver`, `IsLocalization.AtPrime.mem_primesOver_of_isPrime`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `primesOver.isPrime`, `mem_primesOver_iff_mem_normalizedFactors`, `coe_smul_primesOver_eq_map_galRestrict`, `map_algebraMap_eq_finset_prod_pow`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span`, `IsDedekindDomain.primesOverEquivPrimesOver_symm_apply`, `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply`, `Algebra.QuasiFinite.finite_primesOver`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe`, `ncard_primesOver_mul_card_inertia_mul_finrank`, `primesOver.isMaximal`, `comap_fiberIsoOfBijectiveResidueField_symm`, `coe_smul_primesOver`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `IsLocalRing.primesOver_eq`
`under` 📖	CompOp	38 math math: `Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt`, `Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective`, `under_bot`, `under_top`, `ramificationIdx_eq_one_of_isUnramifiedAt`, `AlgHom.IsArithFrobAt.mk_apply`, `map_under_le_under_map`, `under_smul`, `under_under`, `Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt`, `under_map_of_isLocalizationAtPrime`, `liesOver_iff`, `AlgHom.IsArithFrobAt.apply_of_pow_eq_one`, `AlgHom.IsArithFrobAt.restrict_injective`, `Int.absNorm_under_mem`, `Algebra.isUnramifiedAt_iff_of_isDedekindDomain`, `under_def`, `Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt`, `Int.absNorm_under_dvd_absNorm`, `over_under`, `AlgHom.IsArithFrobAt.card_pos`, `Algebra.weaklyQuasiFiniteAt_iff`, `LiesOver.over`, `Polynomial.map_under_lt_comap_of_quasiFiniteAt`, `Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top`, `over_def`, `AlgHom.IsArithFrobAt.restrict_mk`, `under_map_eq_map_under`, `IsPrime.under`, `Int.absNorm_under_eq_sInf`, `under_liesOver_of_liesOver`, `Int.cast_mem_ideal_iff`, `ringChar_quot`, `Int.liesOver_span_absNorm`, `IsMaximal.under`, `Nat.absNorm_under_prime`, `AlgHom.IsArithFrobAt.restrict_apply`, `AlgHom.IsArithFrobAt.finite_quotient`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_liesOver_bot` 📖	mathematical	—	`LiesOver` `CommRing.toCommSemiring` `Ring.toSemiring` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CommSemiring.toSemiring`	—	`under_bot`
`comap_eq_of_scalar_tower_quotient` 📖	mathematical	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Quotient.commSemiring` `Quotient.semiring` `RingHom.instFunLike` `algebraMap`	`comap` `RingHom.instRingHomClass`	—	`IsScalarTower.right` `ext` `RingHom.instRingHomClass` `mem_comap` `instIsTwoSided_1` `Quotient.eq_zero_iff_mem` `Quotient.mk_algebraMap` `IsScalarTower.algebraMap_apply` `Quotient.algebraMap_eq` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`comap_liesOver` 📖	mathematical	—	`LiesOver` `comap` `AlgHomClass.toRingHomClass`	—	`LiesOver.of_eq_comap` `AlgHomClass.toRingHomClass`
`disjoint_primeCompl_of_liesOver` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Submonoid.instSetLike` `Algebra.algebraMapSubmonoid` `primeCompl` `CommSemiring.toSemiring` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHom.instRingHomClass` `coe_comap` `SetLike.ext'_iff` `under_def` `liesOver_iff` `one_notMem` `Submonoid.map.congr_simp` `Set.subset_compl_comm` `Set.instReflSubset`
`eq_top_iff_of_liesOver` 📖	mathematical	—	`Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CommSemiring.toSemiring`	—	`over_def` `comap_eq_top_iff`
`instLiesOverBotOfIsPrime` 📖	mathematical	—	`LiesOver` `Semifield.toCommSemiring` `Field.toSemifield` `Bot.bot` `Ideal` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsSimpleOrder.eq_bot_or_eq_top` `isSimpleOrder` `IsPrime.ne_top'` `IsPrime.under`
`liesOver_iff` 📖	mathematical	—	`LiesOver` `under`	—	—
`map_equiv_liesOver` 📖	mathematical	—	`LiesOver` `map` `EquivLike.toFunLike`	—	`LiesOver.of_eq_map_equiv`
`map_under_le_under_map` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `map` `RingHom` `RingHom.instFunLike` `algebraMap` `under`	—	`le_comap_of_map_le` `map_map` `IsScalarTower.algebraMap_eq` `RingHom.instRingHomClass` `map_le_iff_le_comap` `comap_comap` `comap_mono` `le_comap_map`
`mem_of_liesOver` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`over_def`
`ne_bot_of_liesOver_of_ne_bot` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `over_def` `under_bot`
`ne_bot_of_mem_primesOver` 📖	—	`Ideal` `Ring.toSemiring` `Set` `Set.instMembership` `primesOver` `CommRing.toCommSemiring`	—	—	`ne_bot_of_liesOver_of_ne_bot`
`ne_top_iff_of_liesOver` 📖	—	—	—	—	`Iff.ne` `eq_top_iff_of_liesOver`
`over_def` 📖	mathematical	—	`under`	—	`LiesOver.over`
`over_under` 📖	mathematical	—	`LiesOver` `under`	—	—
`top_liesOver_top` 📖	mathematical	—	`LiesOver` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CommSemiring.toSemiring`	—	`under_top`
`under_bot` 📖	mathematical	—	`under` `CommRing.toCommSemiring` `Ring.toSemiring` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CommSemiring.toSemiring`	—	`comap_bot_of_injective` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero`
`under_def` 📖	mathematical	—	`under` `comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	—
`under_liesOver_of_liesOver` 📖	mathematical	—	`LiesOver` `CommSemiring.toSemiring` `under`	—	`LiesOver.tower_bot` `over_under`
`under_map_eq_map_under` 📖	mathematical	—	`under` `map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`RingHom.instRingHomClass` `IsCoatom.le_iff_eq` `isMaximal_def` `comap_ne_top` `map_under_le_under_map`
`under_smul` 📖	mathematical	—	`under` `Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction`	—	`ext` `mem_comap` `mem_pointwise_smul_iff_inv_smul_mem` `smul_algebraMap`
`under_top` 📖	mathematical	—	`under` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CommSemiring.toSemiring`	—	`comap_top`
`under_under` 📖	mathematical	—	`under` `CommSemiring.toSemiring`	—	`RingHom.instRingHomClass` `comap.congr_simp`

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`under` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `Ideal.under`	—	`comap` `RingHom.instRingHomClass`

Ideal.LiesOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_eq_comap` 📖	mathematical	`Ideal.comap` `AlgHomClass.toRingHomClass`	`Ideal.LiesOver`	—	`AlgHomClass.toRingHomClass` `Ideal.over_def` `AlgHom.algHomClass` `AlgHom.comp_algebraMap`
`of_eq_map_equiv` 📖	mathematical	`Ideal.map` `EquivLike.toFunLike`	`Ideal.LiesOver`	—	`of_eq_comap` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquivClass.toRingEquivClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Ideal.comap_symm`
`over` 📖	mathematical	—	`Ideal.under`	—	—
`smul` 📖	mathematical	—	`Ideal.LiesOver` `Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Ideal.pointwiseDistribMulAction`	—	`over` `Ideal.under_smul`
`tower_bot` 📖	mathematical	—	`Ideal.LiesOver` `CommSemiring.toSemiring`	—	`Ideal.over_def` `Ideal.under_under`
`trans` 📖	mathematical	—	`Ideal.LiesOver`	—	`Ideal.over_def` `Ideal.under_under`

Ideal.Quotient

Definitions

Name	Category	Theorems
`algEquivOfEqComap` 📖	CompOp	1 math math: `algEquivOfEqComap_apply`
`algEquivOfEqMap` 📖	CompOp	1 math math: `algEquivOfEqMap_apply`
`algebraOfLiesOver` 📖	CompOp	25 math math: `exists_algHom_fixedPoint_quotient_under`, `map_ker_stabilizer_subtype`, `Ideal.inertiaDeg_algebraMap`, `algEquivOfEqMap_apply`, `instIsSeparableQuotientIdealOfResidueField`, `instFaithfulSMul`, `algebra_finiteType_of_liesOver`, `stabilizerHom_surjective`, `normal`, `stabilizerHom_surjective_of_profinite`, `stabilizerHom_apply`, `isNoetherian_of_liesOver`, `exists_algEquiv_fixedPoint_quotient_under`, `module_finite_of_liesOver`, `stabilizerQuotientInertiaEquiv_mk`, `algEquivOfEqComap_apply`, `IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply`, `isScalarTower_of_liesOver`, `ker_stabilizerHom`, `algebra_isIntegral_of_liesOver`, `Ideal.card_stabilizer_eq_card_inertia_mul_finrank`, `finite_of_isInvariant`, `Ideal.ncard_primesOver_mul_card_inertia_mul_finrank`, `Algebra.isSeparable_residueField_iff`, `algebraMap_mk_of_liesOver`
`algebraQuotientMapQuotient` 📖	CompOp	12 math math: `IsLocalRing.finrank_quotient_map`, `QuotientMapQuotient.isNoetherian`, `tower_quotient_map_quotient`, `IsLocalRing.basisQuotient_repr`, `algebraMap_quotient_map_quotient`, `Ideal.finrank_quotient_map`, `Algebra.trace_quotient_mk`, `IsLocalRing.quotient_span_eq_top_iff_span_eq_top`, `IsLocalRing.basisQuotient_apply`, `trace_quotient_eq_trace_localization_quotient`, `Algebra.trace_quotient_eq_of_isDedekindDomain`, `mk_smul_mk_quotient_map_quotient`
`stabilizerHom` 📖	CompOp	6 math math: `map_ker_stabilizer_subtype`, `stabilizerHom_surjective`, `stabilizerHom_surjective_of_profinite`, `stabilizerHom_apply`, `stabilizerQuotientInertiaEquiv_mk`, `ker_stabilizerHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivOfEqComap_apply` 📖	mathematical	`Ideal.comap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `commSemiring` `semiring` `algebraOfLiesOver` `AlgEquiv.instFunLike` `algEquivOfEqComap` `RingHom` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `Ideal.instIsTwoSided_1`
`algEquivOfEqMap_apply` 📖	mathematical	`Ideal.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `commSemiring` `semiring` `algebraOfLiesOver` `AlgEquiv.instFunLike` `algEquivOfEqMap` `RingHom` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Ideal.instIsTwoSided_1`
`algebraMap_mk_of_liesOver` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Semiring.toNonAssocSemiring` `commSemiring` `semiring` `RingHom.instFunLike` `algebraMap` `algebraOfLiesOver` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1`
`algebraMap_quotient_map_quotient` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `commSemiring` `semiring` `algebraQuotientMapQuotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1`
`instFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Algebra.toSMul` `commSemiring` `semiring` `algebraOfLiesOver`	—	`faithfulSMul_iff_algebraMap_injective` `Ideal.instIsTwoSided_1` `eq` `Ideal.mem_of_liesOver` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver` 📖	mathematical	—	`Ideal.IsPrime` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `semiring` `ring` `Ideal.instIsTwoSided_1`	—	`Ideal.isPrime_map_quotientMk_of_isPrime` `Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap` `Ideal.LiesOver.over` `le_refl`
`isScalarTower_of_liesOver` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.Quotient.instSMul'` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `IsScalarTower.right` `commSemiring` `semiring` `algebraOfLiesOver`	—	`IsScalarTower.of_algebraMap_eq'` `IsScalarTower.algebraMap_eq`
`ker_stabilizerHom` 📖	mathematical	—	`MonoidHom.ker` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `Ideal.pointwiseDistribMulAction` `Subgroup.toGroup` `AlgEquiv` `HasQuotient.Quotient` `Ideal.instHasQuotient_1` `commSemiring` `semiring` `algebraOfLiesOver` `Monoid.toMulOneClass` `AlgEquiv.aut` `stabilizerHom` `Subgroup.subgroupOf` `Ideal.inertia` `CommRing.toRing` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulSemiringAction.toDistribMulAction`	—	`Subgroup.ext` `Subgroup.instSubgroupClass` `Ideal.instIsTwoSided_1` `Function.Surjective.forall` `mk_surjective`
`map_ker_stabilizer_subtype` 📖	mathematical	—	`Subgroup.map` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `Ideal.pointwiseDistribMulAction` `Subgroup.toGroup` `Subgroup.subtype` `MonoidHom.ker` `AlgEquiv` `HasQuotient.Quotient` `Ideal.instHasQuotient_1` `commSemiring` `semiring` `algebraOfLiesOver` `Monoid.toMulOneClass` `AlgEquiv.aut` `stabilizerHom` `Ideal.inertia` `CommRing.toRing` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulSemiringAction.toDistribMulAction`	—	`Subgroup.instSubgroupClass` `ker_stabilizerHom` `AddSubgroup.inertia_map_subtype` `inf_of_le_left`
`mk_smul_mk_quotient_map_quotient` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Algebra.toSMul` `commSemiring` `semiring` `algebraQuotientMapQuotient` `DFunLike.coe` `ring` `Ideal.instIsTwoSided_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Algebra.smul_def` `Ideal.instIsTwoSided_1`
`nontrivial_of_liesOver_of_isPrime` 📖	mathematical	—	`Nontrivial` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1`	—	`nontrivial_of_liesOver_of_ne_top` `Ideal.IsPrime.ne_top`
`nontrivial_of_liesOver_of_ne_top` 📖	mathematical	—	`Nontrivial` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1`	—	`nontrivial_iff` `Ideal.ne_top_iff_of_liesOver`
`stabilizerHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `commSemiring` `semiring` `algebraOfLiesOver` `AlgEquiv.instFunLike` `MonoidHom` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `Ideal.pointwiseDistribMulAction` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Subgroup.toGroup` `AlgEquiv.aut` `MonoidHom.instFunLike` `stabilizerHom` `RingHom` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Subgroup.instDistribMulActionSubtypeMem` `MulSemiringAction.toDistribMulAction`	—	`Ideal.instIsTwoSided_1`
`tower_quotient_map_quotient` 📖	mathematical	—	`IsScalarTower` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Submodule.Quotient.instSMul` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `commSemiring` `semiring` `algebraQuotientMapQuotient` `Submodule.Quotient.instSMul'` `IsScalarTower.right`	—	`IsScalarTower.of_algebraMap_eq` `Ideal.instIsTwoSided_1` `algebraMap_eq` `algebraMap_quotient_map_quotient` `mk_algebraMap`

Ideal.primesOver

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrime` 📖	mathematical	—	`Ideal.IsPrime` `Ideal` `Set` `Set.instMembership` `Ideal.primesOver`	—	—
`liesOver` 📖	mathematical	—	`Ideal.LiesOver` `Ideal` `Set` `Set.instMembership` `Ideal.primesOver`	—	—

---

← Back to Index