Lattice

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

Statistics

Metric	Count
Definitions	0
Theorems eq_bot_or_top, eq_top_iff_one, eq_top_of_isUnit_mem, eq_top_of_unit_mem, instIsTwoSidedBot, instIsTwoSidedIInf, instIsTwoSidedTop, mem_bot, mem_iInf, mem_iSup_of_mem, mem_inf, mem_sInf, mem_sSup_of_mem, mem_sup_left, mem_sup_right, ne_top_iff_one	16
Total	16

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot_or_top 📖	mathematical	—	Bot.bot Ideal DivisionSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Top.top Submodule.instTop	—	ne_top_iff_one eq_bot_iff inv_mul_cancel₀ mul_mem_left
eq_top_iff_one 📖	mathematical	—	Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eq_top_of_unit_mem mul_one
eq_top_of_isUnit_mem 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Top.top Submodule.instTop	—	IsUnit.exists_left_inv eq_top_of_unit_mem
eq_top_of_unit_mem 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Top.top Submodule.instTop	—	eq_top_iff mul_mem_left mul_assoc mul_one
instIsTwoSidedBot 📖	mathematical	—	IsTwoSided Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	MulZeroClass.zero_mul ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
instIsTwoSidedIInf 📖	mathematical	IsTwoSided	iInf Ideal Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Submodule.mem_iInf mul_mem_right
instIsTwoSidedTop 📖	mathematical	—	IsTwoSided Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
mem_bot 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Submodule.instBot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Submodule.mem_bot
mem_iInf 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iInf Submodule.instInfSet	—	Submodule.mem_iInf
mem_iSup_of_mem 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	le_iSup
mem_inf 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instMin	—	—
mem_sInf 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule InfSet.sInf Submodule.instInfSet	—	iInf_pos
mem_sSup_of_mem 📖	mathematical	Ideal Set Set.instMembership SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	le_sSup
mem_sup_left 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	le_sup_left
mem_sup_right 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	le_sup_right
ne_top_iff_one 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eq_top_iff_one

---

← Back to Index