Colon

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

Statistics

Metric	Count
Definitions colon	1
Theorems annihilator_quotient, colon_span, le_colon, mem_colon_span_singleton, annihilator_map_mkQ_eq_colon, annihilator_quotient, bot_colon, bot_colon', colon_bot, colon_empty, colon_eq_top_iff_subset, colon_finsetInf, colon_iUnion, colon_inf_eq_left_of_subset, colon_mono, colon_singleton_zero, colon_span, colon_top, colon_union, colon_univ, iInf_colon, iInf_colon_iSup, iInf_colon_iUnion, inf_colon, instIsTwoSidedColonCoe, mem_colon, mem_colon', mem_colon_iff_le, mem_colon_singleton, mem_colon_span_singleton, top_colon	31
Total	32

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_quotient 📖	mathematical	—	Module.annihilator HasQuotient.Quotient Ideal Ring.toSemiring Submodule.hasQuotient Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid Submodule.Quotient.addCommGroup Submodule.Quotient.module	—	Submodule.annihilator_quotient Submodule.colon_univ
colon_span 📖	mathematical	—	Submodule.colon CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.coe Ideal Submodule.setLike span	—	Submodule.colon_span
le_colon 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.colon	—	Eq.trans_le Submodule.colon_univ Submodule.colon_mono le_rfl Set.subset_univ
mem_colon_span_singleton 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.colon SetLike.coe span Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	colon_span

Submodule

Definitions

Name	Category	Theorems
colon 📖	CompOp	52 math math: colon_empty, mem_colon_span_singleton, IdealFilter.IsUniform.colon_mem, annihilator_quotient, mem_colon', Ideal.mem_colon_span_singleton, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, IsPrimary.radical_colon_singleton_of_notMem, exists_le_isAssociatedPrime_of_isNoetherianRing, colon_finsetInf, isAssociatedPrime_def, iInf_colon_iSup, colon_union, IsPrimary.isPrime_radical_colon, IsMinimalPrimaryDecomposition.mem_associatedPrimes, instIsTwoSidedColonCoe, IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes, isAssociatedPrime_iff, annihilator_map_mkQ_eq_colon, top_colon, mem_colon_iff_le, IsMinimalPrimaryDecomposition.distinct, colon_span, colon_eq_top_iff_subset, colon_singleton_zero, IsPrimary.radical_colon_singleton_eq_ite, colon_univ, IsMinimalPrimaryDecomposition.injOn, isPrimary_decomposition_pairwise_ne_radical, bot_colon', isQuotientEquivQuotientPrime_iff, colon_mono, exists_eq_colon_of_mem_minimalPrimes, iInf_colon, Ideal.colon_span, iInf_colon_iUnion, exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, mem_colon_singleton, colon_top, mem_colon, IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff, isAssociatedPrime_iff, Ideal.isPrimary_decomposition_pairwise_ne_radical, colon_iUnion, inf_colon, IdealFilter.isTorsionQuot_def, IsAssociatedPrime.eq_radical_colon, bot_colon, colon_bot, IsPrimary.mem_or_mem, colon_inf_eq_left_of_subset, Ideal.le_colon

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annihilator_map_mkQ_eq_colon 📖	mathematical	—	annihilator HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ colon SetLike.coe setLike	—	Ideal.ext RingHomSurjective.ids mem_annihilator mem_colon Quotient.mk_eq_zero mem_map_of_mem
annihilator_quotient 📖	mathematical	—	Module.annihilator HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module colon Set.univ	—	Ideal.ext RingHomSurjective.ids map_top LinearMap.range_eq_top mkQ_surjective annihilator_top annihilator_map_mkQ_eq_colon top_coe
bot_colon 📖	mathematical	—	colon Bot.bot Submodule instBot SetLike.coe setLike annihilator	—	Ideal.ext
bot_colon' 📖	mathematical	—	colon CommSemiring.toSemiring Bot.bot Submodule instBot annihilator span	—	Ideal.ext
colon_bot 📖	mathematical	—	colon SetLike.coe Submodule setLike Bot.bot instBot Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	AddSubmonoidClass.toZeroMemClass addSubmonoidClass
colon_empty 📖	mathematical	—	colon Set Set.instEmptyCollection Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
colon_eq_top_iff_subset 📖	mathematical	—	colon Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instHasSubset SetLike.coe Submodule setLike	—	one_smul
colon_finsetInf 📖	mathematical	—	colon Finset.inf Submodule Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instOrderTop Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext
colon_iUnion 📖	mathematical	—	colon Set.iUnion iInf Ideal instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext
colon_inf_eq_left_of_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe Submodule setLike	colon Submodule instMin	—	Ideal.ext SMulMemClass.smul_mem smulMemClass
colon_mono 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Set.instHasSubset	Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule colon	—	mem_colon
colon_singleton_zero 📖	mathematical	—	colon Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Top.top Ideal instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	AddSubmonoidClass.toZeroMemClass addSubmonoidClass
colon_span 📖	mathematical	—	colon CommSemiring.toSemiring SetLike.coe Submodule setLike span	—	LE.le.antisymm colon_mono le_rfl subset_span mem_colon span_induction smul_zero AddSubmonoidClass.toZeroMemClass addSubmonoidClass smul_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SMulCommClass.smul_comm smulCommClass_self
colon_top 📖	mathematical	—	colon NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set.univ	—	colon_univ
colon_union 📖	mathematical	—	colon Set Set.instUnion Ideal instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext
colon_univ 📖	mathematical	—	colon NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set.univ	—	mul_one Ideal.mul_mem_right
iInf_colon 📖	mathematical	—	colon iInf Submodule instInfSet Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext
iInf_colon_iSup 📖	mathematical	—	colon iInf Submodule instInfSet Set.iUnion Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	iInf_colon_iUnion
iInf_colon_iUnion 📖	mathematical	—	colon iInf Submodule instInfSet Set.iUnion Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext
inf_colon 📖	mathematical	—	colon Submodule instMin Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext
instIsTwoSidedColonCoe 📖	mathematical	—	Ideal.IsTwoSided colon SetLike.coe Submodule setLike	—	smul_mem SemigroupAction.mul_smul
mem_colon 📖	mathematical	—	Ideal SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule colon Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.smul_set_subset_iff
mem_colon' 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule colon Set Set.instLE SetLike.coe Submodule 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	—	mem_colon
mem_colon_iff_le 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule colon SetLike.coe Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid	—	—
mem_colon_singleton 📖	mathematical	—	Ideal SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule colon Set Set.instSingletonSet Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
mem_colon_span_singleton 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule colon SetLike.coe Submodule span Set Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	colon_span
top_colon 📖	mathematical	—	colon Top.top Submodule instTop Ideal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—

---

← Back to Index