Lattice

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

Statistics

Metric	Count
Definitions `instBot`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instCompleteSemilatticeSup`, `instInfSet`, `instSemilatticeInf`, `instSemilatticeSup`, `instSupSet`, `instTop`	9
Theorems `bot_ringCon`, `coe_bot`, `coe_top`, `eq_top`, `iInf_ringCon`, `iSup_ringCon`, `inf_ringCon`, `mem_bot`, `mem_iInf`, `mem_inf`, `mem_sInf`, `mem_sup`, `mem_sup_left`, `mem_sup_right`, `mem_top`, `one_mem`, `one_mem_iff`, `sInf_ringCon`, `sSup_ringCon`, `sup_ringCon`, `top_ringCon`	21
Total	30

TwoSidedIdeal

Definitions

Name	Category	Theorems
`instBot` 📖	CompOp	7 math math: `matrix_jacobson_bot`, `bot_asIdeal`, `matrix_bot`, `ker_eq_bot`, `coe_bot`, `bot_ringCon`, `mem_bot`
`instCompleteLattice` 📖	CompOp	2 math math: `isSimpleRing_iff`, `IsSimpleRing.simple`
`instCompleteSemilatticeInf` 📖	CompOp	—
`instCompleteSemilatticeSup` 📖	CompOp	—
`instInfSet` 📖	CompOp	4 math math: `mem_iInf`, `iInf_ringCon`, `sInf_ringCon`, `mem_sInf`
`instSemilatticeInf` 📖	CompOp	2 math math: `mem_inf`, `inf_ringCon`
`instSemilatticeSup` 📖	CompOp	4 math math: `mem_sup_right`, `mem_sup`, `sup_ringCon`, `mem_sup_left`
`instSupSet` 📖	CompOp	2 math math: `iSup_ringCon`, `sSup_ringCon`
`instTop` 📖	CompOp	10 math math: `one_mem_iff`, `coe_top`, `compactlySupported_eq_top_of_isCompact`, `matrix_top`, `compactlySupported_eq_top`, `compactlySupported_eq_top_iff`, `eq_top`, `mem_top`, `top_asIdeal`, `top_ringCon`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_ringCon` 📖	mathematical	—	`ringCon` `Bot.bot` `TwoSidedIdeal` `instBot` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `RingCon.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`coe_bot` 📖	mathematical	—	`SetLike.coe` `TwoSidedIdeal` `setLike` `Bot.bot` `instBot` `Set` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TwoSidedIdeal` `setLike` `Top.top` `instTop` `Set.univ`	—	—
`eq_top` 📖	mathematical	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `setLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	`Top.top` `instTop`	—	`one_mem_iff`
`iInf_ringCon` 📖	mathematical	—	`ringCon` `iInf` `TwoSidedIdeal` `instInfSet` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `RingCon.instInfSet`	—	`Set.ext`
`iSup_ringCon` 📖	mathematical	—	`ringCon` `iSup` `TwoSidedIdeal` `instSupSet` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `RingCon.instCompleteLattice`	—	`Set.ext`
`inf_ringCon` 📖	mathematical	—	`ringCon` `TwoSidedIdeal` `SemilatticeInf.toMin` `instSemilatticeInf` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `RingCon.instCompleteLattice`	—	—
`mem_bot` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `Bot.bot` `instBot` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`mem_iInf` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `iInf` `instInfSet`	—	—
`mem_inf` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `SemilatticeInf.toMin` `instSemilatticeInf`	—	—
`mem_sInf` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `InfSet.sInf` `instInfSet`	—	—
`mem_sup` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `instSemilatticeSup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`zero_mem` `zero_add` `add_mem` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `Mathlib.Tactic.Abel.const_add_termg` `neg_mem` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `mul_mem_left` `mul_add` `Distrib.leftDistribClass` `mul_mem_right` `add_mul` `Distrib.rightDistribClass` `sup_le` `rel_iff` `mem_mk'` `add_zero` `sub_zero` `mem_sup_left` `mem_sup_right`
`mem_sup_left` 📖	mathematical	`TwoSidedIdeal` `SetLike.instMembership` `setLike`	`SemilatticeSup.toMax` `instSemilatticeSup`	—	`le_sup_left`
`mem_sup_right` 📖	mathematical	`TwoSidedIdeal` `SetLike.instMembership` `setLike`	`SemilatticeSup.toMax` `instSemilatticeSup`	—	`le_sup_right`
`mem_top` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `Top.top` `instTop`	—	—
`one_mem` 📖	mathematical	`Top.top` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `instTop`	`SetLike.instMembership` `setLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`one_mem_iff`
`one_mem_iff` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `setLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Top.top` `instTop`	—	`eq_top_iff` `mul_one` `mul_mem_left`
`sInf_ringCon` 📖	mathematical	—	`ringCon` `InfSet.sInf` `TwoSidedIdeal` `instInfSet` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `RingCon.instInfSet` `Set.image`	—	—
`sSup_ringCon` 📖	mathematical	—	`ringCon` `SupSet.sSup` `TwoSidedIdeal` `instSupSet` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `RingCon.instCompleteLattice` `Set.image`	—	—
`sup_ringCon` 📖	mathematical	—	`ringCon` `TwoSidedIdeal` `SemilatticeSup.toMax` `instSemilatticeSup` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `RingCon.instCompleteLattice`	—	—
`top_ringCon` 📖	mathematical	—	`ringCon` `Top.top` `TwoSidedIdeal` `instTop` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toMul` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `RingCon.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—

---

← Back to Index