Documentation Verification Report

Saturation

📁 Source: Mathlib/Algebra/Group/Submonoid/Saturation.lean

Statistics

Metric	Count
Definitions `AddSaturated`, `giSaturation`, `saturation`, `SaturatedAddSubmonoid`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instInfSet`, `instMin`, `instPartialOrder`, `instSetLike`, `instTop`, `toAddSubmonoid`, `SaturatedSubmonoid`, `instCompleteLattice`, `instCompleteSemilatticeInf`, `instInfSet`, `instMin`, `instPartialOrder`, `instSetLike`, `instTop`, `toSubmonoid`, `MulSaturated`, `giSaturation`, `saturation`	24
Theorems `add_mem_iff`, `iInf`, `inf`, `of_left`, `of_right`, `sInf`, `top`, `gc_saturation`, `le_toAddSubmonoid_saturation`, `mem_saturation_iff`, `mem_saturation_iff'`, `saturation_bot`, `saturation_iSup`, `saturation_induction`, `saturation_le_iff_le`, `saturation_le_of_le`, `saturation_sSup`, `saturation_sup`, `saturation_toAddSubmonoid`, `saturation_top`, `addSaturated`, `bot_def`, `ext`, `ext'`, `ext_iff`, `iSup_def`, `instAddSubmonoidClass`, `mem_bot_iff`, `mem_sInf`, `mem_toAddSubmonoid`, `mem_top`, `sSup_def`, `sup_def`, `toAddSubmonoid_injective`, `bot_def`, `ext`, `ext'`, `ext_iff`, `iSup_def`, `instSubmonoidClass`, `mem_bot_iff`, `mem_sInf`, `mem_toSubmonoid`, `mem_top`, `mulSaturated`, `sSup_def`, `sup_def`, `toSubmonoid_injective`, `iInf`, `inf`, `mul_mem_iff`, `of_left`, `of_right`, `sInf`, `top`, `gc_saturation`, `le_toSubmonoid_saturation`, `mem_saturation_iff`, `mem_saturation_iff'`, `mem_saturation_iff_exists_dvd`, `saturation_bot`, `saturation_iSup`, `saturation_induction`, `saturation_le_iff_le`, `saturation_le_of_le`, `saturation_sSup`, `saturation_sup`, `saturation_toSubmonoid`, `saturation_top`	69
Total	93

AddSubmonoid

Definitions

Name	Category	Theorems
`AddSaturated` 📖	MathDef	7 math math: `AddSaturated.of_left`, `AddSaturated.sInf`, `AddSaturated.iInf`, `AddSaturated.inf`, `SaturatedAddSubmonoid.addSaturated`, `AddSaturated.of_right`, `AddSaturated.top`
`giSaturation` 📖	CompOp	—
`saturation` 📖	CompOp	16 math math: `gc_saturation`, `le_toAddSubmonoid_saturation`, `saturation_le_of_le`, `saturation_toAddSubmonoid`, `saturation_top`, `SaturatedAddSubmonoid.sSup_def`, `mem_saturation_iff`, `SaturatedAddSubmonoid.sup_def`, `saturation_iSup`, `SaturatedAddSubmonoid.bot_def`, `saturation_sSup`, `SaturatedAddSubmonoid.iSup_def`, `saturation_sup`, `mem_saturation_iff'`, `saturation_bot`, `saturation_le_iff_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gc_saturation` 📖	mathematical	—	`GaloisConnection` `AddSubmonoid` `SaturatedAddSubmonoid` `PartialOrder.toPreorder` `instPartialOrder` `SaturatedAddSubmonoid.instPartialOrder` `saturation` `SaturatedAddSubmonoid.toAddSubmonoid`	—	`SaturatedAddSubmonoid.mem_sInf`
`le_toAddSubmonoid_saturation` 📖	mathematical	—	`AddSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SaturatedAddSubmonoid.toAddSubmonoid` `saturation`	—	`GaloisConnection.le_u_l` `gc_saturation`
`mem_saturation_iff` 📖	mathematical	—	`SaturatedAddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `SaturatedAddSubmonoid.instSetLike` `saturation` `AddSubmonoid` `instSetLike` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`saturation_induction` `add_zero` `add_add_add_comm` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `instAddSubmonoidClass` `add_assoc` `add_left_comm` `SaturatedAddSubmonoid.addSaturated` `le_toAddSubmonoid_saturation`
`mem_saturation_iff'` 📖	mathematical	—	`SaturatedAddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `SaturatedAddSubmonoid.instSetLike` `saturation` `AddSubmonoid` `instSetLike` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`mem_saturation_iff` `add_comm`
`saturation_bot` 📖	mathematical	—	`saturation` `Bot.bot` `AddSubmonoid` `instBot` `SaturatedAddSubmonoid` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `SaturatedAddSubmonoid.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `gc_saturation`
`saturation_iSup` 📖	mathematical	—	`saturation` `iSup` `AddSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `SaturatedAddSubmonoid` `SaturatedAddSubmonoid.instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_saturation`
`saturation_induction` 📖	—	`le_toAddSubmonoid_saturation` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMemClass.add_mem` `SaturatedAddSubmonoid` `SaturatedAddSubmonoid.instSetLike` `AddSubmonoidClass.toAddMemClass` `SaturatedAddSubmonoid.instAddSubmonoidClass` `saturation` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `SaturatedAddSubmonoid.toAddSubmonoid` `SaturatedAddSubmonoid.addSaturated`	—	—	`le_toAddSubmonoid_saturation` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SaturatedAddSubmonoid.instAddSubmonoidClass` `SaturatedAddSubmonoid.addSaturated` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `instAddSubmonoidClass` `SaturatedAddSubmonoid.mem_sInf`
`saturation_le_iff_le` 📖	mathematical	—	`SaturatedAddSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SaturatedAddSubmonoid.instPartialOrder` `saturation` `AddSubmonoid` `instPartialOrder` `SaturatedAddSubmonoid.toAddSubmonoid`	—	`gc_saturation`
`saturation_le_of_le` 📖	mathematical	`AddSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SaturatedAddSubmonoid.toAddSubmonoid`	`SaturatedAddSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SaturatedAddSubmonoid.instPartialOrder` `saturation`	—	`saturation_le_iff_le`
`saturation_sSup` 📖	mathematical	—	`saturation` `SupSet.sSup` `AddSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `iSup` `SaturatedAddSubmonoid` `SaturatedAddSubmonoid.instCompleteLattice` `Set` `Set.instMembership`	—	`GaloisConnection.l_sSup` `gc_saturation`
`saturation_sup` 📖	mathematical	—	`saturation` `AddSubmonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `SaturatedAddSubmonoid` `SaturatedAddSubmonoid.instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_saturation`
`saturation_toAddSubmonoid` 📖	mathematical	—	`saturation` `SaturatedAddSubmonoid.toAddSubmonoid`	—	`GaloisInsertion.l_u_eq`
`saturation_top` 📖	mathematical	—	`saturation` `Top.top` `AddSubmonoid` `instTop` `SaturatedAddSubmonoid` `SaturatedAddSubmonoid.instTop`	—	`GaloisInsertion.l_top`

AddSubmonoid.AddSaturated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem_iff` 📖	mathematical	`AddSubmonoid.AddSaturated`	`AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubmonoid.instAddSubmonoidClass`
`iInf` 📖	mathematical	`AddSubmonoid.AddSaturated`	`AddSubmonoid.AddSaturated` `iInf` `AddSubmonoid` `AddSubmonoid.instInfSet`	—	`sInf` `Set.forall_mem_range`
`inf` 📖	mathematical	`AddSubmonoid.AddSaturated`	`AddSubmonoid.AddSaturated` `AddSubmonoid` `AddSubmonoid.instMin`	—	—
`of_left` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddSubmonoid.AddSaturated` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`add_comm`
`of_right` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddSubmonoid.AddSaturated` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`of_left` `add_comm`
`sInf` 📖	mathematical	`AddSubmonoid.AddSaturated`	`AddSubmonoid.AddSaturated` `InfSet.sInf` `AddSubmonoid` `AddSubmonoid.instInfSet`	—	`AddSubmonoid.mem_sInf`
`top` 📖	mathematical	—	`AddSubmonoid.AddSaturated` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop`	—	—

SaturatedAddSubmonoid

Definitions

Name	Category	Theorems
`instCompleteLattice` 📖	CompOp	9 math math: `sSup_def`, `sup_def`, `AddSubmonoid.saturation_iSup`, `bot_def`, `AddSubmonoid.saturation_sSup`, `iSup_def`, `AddSubmonoid.saturation_sup`, `AddSubmonoid.saturation_bot`, `mem_bot_iff`
`instCompleteSemilatticeInf` 📖	CompOp	—
`instInfSet` 📖	CompOp	1 math math: `mem_sInf`
`instMin` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	3 math math: `AddSubmonoid.gc_saturation`, `AddSubmonoid.saturation_le_of_le`, `AddSubmonoid.saturation_le_iff_le`
`instSetLike` 📖	CompOp	7 math math: `mem_toAddSubmonoid`, `instAddSubmonoidClass`, `AddSubmonoid.mem_saturation_iff`, `mem_sInf`, `AddSubmonoid.mem_saturation_iff'`, `mem_top`, `mem_bot_iff`
`instTop` 📖	CompOp	2 math math: `AddSubmonoid.saturation_top`, `mem_top`
`toAddSubmonoid` 📖	CompOp	11 math math: `AddSubmonoid.gc_saturation`, `AddSubmonoid.le_toAddSubmonoid_saturation`, `mem_toAddSubmonoid`, `AddSubmonoid.saturation_toAddSubmonoid`, `sSup_def`, `sup_def`, `ext_iff`, `addSaturated`, `iSup_def`, `AddSubmonoid.saturation_le_iff_le`, `toAddSubmonoid_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSaturated` 📖	mathematical	—	`AddSubmonoid.AddSaturated` `toAddSubmonoid`	—	—
`bot_def` 📖	mathematical	—	`Bot.bot` `SaturatedAddSubmonoid` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `AddSubmonoid.saturation` `AddSubmonoid` `AddSubmonoid.instBot`	—	—
`ext` 📖	—	`toAddSubmonoid`	—	—	`toAddSubmonoid_injective`
`ext'` 📖	—	`SaturatedAddSubmonoid` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`toAddSubmonoid`	—	`ext`
`iSup_def` 📖	mathematical	—	`iSup` `SaturatedAddSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `AddSubmonoid.saturation` `AddSubmonoid` `AddSubmonoid.instCompleteLattice` `toAddSubmonoid`	—	`GaloisInsertion.l_iSup_u`
`instAddSubmonoidClass` 📖	mathematical	—	`AddSubmonoidClass` `SaturatedAddSubmonoid` `instSetLike`	—	`AddSubmonoid.add_mem` `AddSubmonoid.zero_mem`
`mem_bot_iff` 📖	mathematical	—	`SaturatedAddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsAddUnit`	—	`AddSubmonoid.mem_saturation_iff` `AddSubmonoid.mem_bot` `isAddUnit_iff_exists_neg` `instIsDedekindFiniteAddMonoid`
`mem_sInf` 📖	mathematical	—	`SaturatedAddSubmonoid` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`mem_toAddSubmonoid` 📖	mathematical	—	`AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `toAddSubmonoid` `SaturatedAddSubmonoid` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`SaturatedAddSubmonoid` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	—
`sSup_def` 📖	mathematical	—	`SupSet.sSup` `SaturatedAddSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `AddSubmonoid.saturation` `AddSubmonoid` `AddSubmonoid.instCompleteLattice` `Set.image` `toAddSubmonoid`	—	—
`sup_def` 📖	mathematical	—	`SaturatedAddSubmonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `AddSubmonoid.saturation` `AddSubmonoid` `AddSubmonoid.instCompleteLattice` `toAddSubmonoid`	—	—
`toAddSubmonoid_injective` 📖	mathematical	—	`SaturatedAddSubmonoid` `AddSubmonoid` `toAddSubmonoid`	—	—

SaturatedSubmonoid

Definitions

Name	Category	Theorems
`instCompleteLattice` 📖	CompOp	9 math math: `Submonoid.saturation_iSup`, `iSup_def`, `bot_def`, `mem_bot_iff`, `sup_def`, `Submonoid.saturation_bot`, `Submonoid.saturation_sSup`, `sSup_def`, `Submonoid.saturation_sup`
`instCompleteSemilatticeInf` 📖	CompOp	—
`instInfSet` 📖	CompOp	1 math math: `mem_sInf`
`instMin` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	3 math math: `Submonoid.saturation_le_of_le`, `Submonoid.saturation_le_iff_le`, `Submonoid.gc_saturation`
`instSetLike` 📖	CompOp	8 math math: `mem_sInf`, `mem_toSubmonoid`, `instSubmonoidClass`, `Submonoid.mem_saturation_iff_exists_dvd`, `mem_bot_iff`, `Submonoid.mem_saturation_iff'`, `mem_top`, `Submonoid.mem_saturation_iff`
`instTop` 📖	CompOp	2 math math: `Submonoid.saturation_top`, `mem_top`
`toSubmonoid` 📖	CompOp	11 math math: `iSup_def`, `mulSaturated`, `mem_toSubmonoid`, `ext_iff`, `Submonoid.le_toSubmonoid_saturation`, `toSubmonoid_injective`, `Submonoid.saturation_toSubmonoid`, `sup_def`, `sSup_def`, `Submonoid.saturation_le_iff_le`, `Submonoid.gc_saturation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_def` 📖	mathematical	—	`Bot.bot` `SaturatedSubmonoid` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Submonoid.saturation` `Submonoid` `Submonoid.instBot`	—	—
`ext` 📖	—	`toSubmonoid`	—	—	`toSubmonoid_injective`
`ext'` 📖	—	`SaturatedSubmonoid` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`toSubmonoid`	—	`ext`
`iSup_def` 📖	mathematical	—	`iSup` `SaturatedSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Submonoid.saturation` `Submonoid` `Submonoid.instCompleteLattice` `toSubmonoid`	—	`GaloisInsertion.l_iSup_u`
`instSubmonoidClass` 📖	mathematical	—	`SubmonoidClass` `SaturatedSubmonoid` `instSetLike`	—	`Submonoid.mul_mem` `Submonoid.one_mem`
`mem_bot_iff` 📖	mathematical	—	`SaturatedSubmonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsUnit`	—	`instIsDedekindFiniteMonoid`
`mem_sInf` 📖	mathematical	—	`SaturatedSubmonoid` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`mem_toSubmonoid` 📖	mathematical	—	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `toSubmonoid` `SaturatedSubmonoid` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`SaturatedSubmonoid` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	—
`mulSaturated` 📖	mathematical	—	`Submonoid.MulSaturated` `toSubmonoid`	—	—
`sSup_def` 📖	mathematical	—	`SupSet.sSup` `SaturatedSubmonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Submonoid.saturation` `Submonoid` `Submonoid.instCompleteLattice` `Set.image` `toSubmonoid`	—	—
`sup_def` 📖	mathematical	—	`SaturatedSubmonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Submonoid.saturation` `Submonoid` `Submonoid.instCompleteLattice` `toSubmonoid`	—	—
`toSubmonoid_injective` 📖	mathematical	—	`SaturatedSubmonoid` `Submonoid` `toSubmonoid`	—	—

Submonoid

Definitions

Name	Category	Theorems
`MulSaturated` 📖	MathDef	7 math math: `SaturatedSubmonoid.mulSaturated`, `MulSaturated.inf`, `MulSaturated.iInf`, `MulSaturated.top`, `MulSaturated.sInf`, `MulSaturated.of_left`, `MulSaturated.of_right`
`giSaturation` 📖	CompOp	—
`saturation` 📖	CompOp	17 math math: `saturation_iSup`, `SaturatedSubmonoid.iSup_def`, `mem_saturation_iff_exists_dvd`, `le_toSubmonoid_saturation`, `SaturatedSubmonoid.bot_def`, `saturation_toSubmonoid`, `mem_saturation_iff'`, `saturation_le_of_le`, `SaturatedSubmonoid.sup_def`, `saturation_top`, `saturation_bot`, `saturation_sSup`, `SaturatedSubmonoid.sSup_def`, `saturation_le_iff_le`, `mem_saturation_iff`, `gc_saturation`, `saturation_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gc_saturation` 📖	mathematical	—	`GaloisConnection` `Submonoid` `SaturatedSubmonoid` `PartialOrder.toPreorder` `instPartialOrder` `SaturatedSubmonoid.instPartialOrder` `saturation` `SaturatedSubmonoid.toSubmonoid`	—	`SaturatedSubmonoid.mem_sInf`
`le_toSubmonoid_saturation` 📖	mathematical	—	`Submonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SaturatedSubmonoid.toSubmonoid` `saturation`	—	`GaloisConnection.le_u_l` `gc_saturation`
`mem_saturation_iff` 📖	mathematical	—	`SaturatedSubmonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `SaturatedSubmonoid.instSetLike` `saturation` `Submonoid` `instSetLike` `MulOne.toMul` `MulOneClass.toMulOne`	—	`saturation_induction` `mul_one` `mul_mul_mul_comm` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `instSubmonoidClass` `mul_assoc` `mul_left_comm` `SaturatedSubmonoid.mulSaturated` `le_toSubmonoid_saturation`
`mem_saturation_iff'` 📖	mathematical	—	`SaturatedSubmonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `SaturatedSubmonoid.instSetLike` `saturation` `Submonoid` `instSetLike` `MulOne.toMul` `MulOneClass.toMulOne`	—	`mul_comm`
`mem_saturation_iff_exists_dvd` 📖	mathematical	—	`SaturatedSubmonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `SaturatedSubmonoid.instSetLike` `saturation` `Submonoid` `instSetLike` `semigroupDvd` `Monoid.toSemigroup`	—	—
`saturation_bot` 📖	mathematical	—	`saturation` `Bot.bot` `Submonoid` `instBot` `SaturatedSubmonoid` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `SaturatedSubmonoid.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `gc_saturation`
`saturation_iSup` 📖	mathematical	—	`saturation` `iSup` `Submonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `SaturatedSubmonoid` `SaturatedSubmonoid.instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_saturation`
`saturation_induction` 📖	—	`le_toSubmonoid_saturation` `MulOne.toMul` `MulOneClass.toMulOne` `MulMemClass.mul_mem` `SaturatedSubmonoid` `SaturatedSubmonoid.instSetLike` `SubmonoidClass.toMulMemClass` `SaturatedSubmonoid.instSubmonoidClass` `saturation` `Submonoid` `SetLike.instMembership` `instSetLike` `SaturatedSubmonoid.toSubmonoid` `SaturatedSubmonoid.mulSaturated`	—	—	`le_toSubmonoid_saturation` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SaturatedSubmonoid.instSubmonoidClass` `SaturatedSubmonoid.mulSaturated` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `instSubmonoidClass` `SaturatedSubmonoid.mem_sInf`
`saturation_le_iff_le` 📖	mathematical	—	`SaturatedSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SaturatedSubmonoid.instPartialOrder` `saturation` `Submonoid` `instPartialOrder` `SaturatedSubmonoid.toSubmonoid`	—	`gc_saturation`
`saturation_le_of_le` 📖	mathematical	`Submonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SaturatedSubmonoid.toSubmonoid`	`SaturatedSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SaturatedSubmonoid.instPartialOrder` `saturation`	—	`saturation_le_iff_le`
`saturation_sSup` 📖	mathematical	—	`saturation` `SupSet.sSup` `Submonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `iSup` `SaturatedSubmonoid` `SaturatedSubmonoid.instCompleteLattice` `Set` `Set.instMembership`	—	`GaloisConnection.l_sSup` `gc_saturation`
`saturation_sup` 📖	mathematical	—	`saturation` `Submonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `SaturatedSubmonoid` `SaturatedSubmonoid.instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_saturation`
`saturation_toSubmonoid` 📖	mathematical	—	`saturation` `SaturatedSubmonoid.toSubmonoid`	—	`GaloisInsertion.l_u_eq`
`saturation_top` 📖	mathematical	—	`saturation` `Top.top` `Submonoid` `instTop` `SaturatedSubmonoid` `SaturatedSubmonoid.instTop`	—	`GaloisInsertion.l_top`

Submonoid.MulSaturated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf` 📖	mathematical	`Submonoid.MulSaturated`	`Submonoid.MulSaturated` `iInf` `Submonoid` `Submonoid.instInfSet`	—	`sInf` `Set.forall_mem_range`
`inf` 📖	mathematical	`Submonoid.MulSaturated`	`Submonoid.MulSaturated` `Submonoid` `Submonoid.instMin`	—	—
`mul_mem_iff` 📖	mathematical	`Submonoid.MulSaturated`	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `MulOne.toMul` `MulOneClass.toMulOne`	—	`MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass`
`of_left` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`Submonoid.MulSaturated` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`mul_comm`
`of_right` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`Submonoid.MulSaturated` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`of_left` `mul_comm`
`sInf` 📖	mathematical	`Submonoid.MulSaturated`	`Submonoid.MulSaturated` `InfSet.sInf` `Submonoid` `Submonoid.instInfSet`	—	—
`top` 📖	mathematical	—	`Submonoid.MulSaturated` `Top.top` `Submonoid` `Submonoid.instTop`	—	—

(root)

Definitions

Name	Category	Theorems
`SaturatedAddSubmonoid` 📖	CompData	20 math math: `AddSubmonoid.gc_saturation`, `AddSubmonoid.saturation_le_of_le`, `SaturatedAddSubmonoid.mem_toAddSubmonoid`, `SaturatedAddSubmonoid.instAddSubmonoidClass`, `AddSubmonoid.saturation_top`, `SaturatedAddSubmonoid.sSup_def`, `AddSubmonoid.mem_saturation_iff`, `SaturatedAddSubmonoid.mem_sInf`, `SaturatedAddSubmonoid.sup_def`, `AddSubmonoid.saturation_iSup`, `SaturatedAddSubmonoid.bot_def`, `AddSubmonoid.saturation_sSup`, `SaturatedAddSubmonoid.iSup_def`, `AddSubmonoid.saturation_sup`, `AddSubmonoid.mem_saturation_iff'`, `SaturatedAddSubmonoid.mem_top`, `AddSubmonoid.saturation_bot`, `SaturatedAddSubmonoid.mem_bot_iff`, `AddSubmonoid.saturation_le_iff_le`, `SaturatedAddSubmonoid.toAddSubmonoid_injective`
`SaturatedSubmonoid` 📖	CompData	21 math math: `Submonoid.saturation_iSup`, `SaturatedSubmonoid.iSup_def`, `SaturatedSubmonoid.mem_sInf`, `SaturatedSubmonoid.mem_toSubmonoid`, `SaturatedSubmonoid.instSubmonoidClass`, `Submonoid.mem_saturation_iff_exists_dvd`, `SaturatedSubmonoid.toSubmonoid_injective`, `SaturatedSubmonoid.bot_def`, `SaturatedSubmonoid.mem_bot_iff`, `Submonoid.mem_saturation_iff'`, `Submonoid.saturation_le_of_le`, `SaturatedSubmonoid.sup_def`, `Submonoid.saturation_top`, `Submonoid.saturation_bot`, `Submonoid.saturation_sSup`, `SaturatedSubmonoid.sSup_def`, `SaturatedSubmonoid.mem_top`, `Submonoid.saturation_le_iff_le`, `Submonoid.mem_saturation_iff`, `Submonoid.gc_saturation`, `Submonoid.saturation_sup`

---

← Back to Index