Documentation Verification Report

Finiteness

📁 Source: Mathlib/GroupTheory/Finiteness.lean

Statistics

Metric	Count
Definitions	0
Theorems `fg_of_wellQuasiOrderedLE`, `out`, `closure_finite_fg`, `closure_finset_fg`, `fg_def`, `fg_iff`, `fg_iff'`, `fg_iff_addMonoid_fg`, `fg_iff_addSubgroup_fg`, `fg_iff_exists_freeAddGroup_hom_surjective`, `fg_iff_mul_fg`, `fg_of_finite`, `fg_of_group_fg`, `fg_of_surjective`, `fg_range`, `instFGInt`, `fg_top`, `closure_finite_fg`, `closure_finset_fg`, `fG_iff`, `fg_def`, `fg_iff`, `fg_iff_addSubmonoid_fg`, `fg_iff_exists_freeAddMonoid_hom_surjective`, `fg_iff_mul_fg`, `fg_of_addGroup_fg`, `fg_of_finite`, `fg_of_monoid_fg`, `fg_of_surjective`, `fg_range`, `instFGNat`, `multiples_fg`, `biSup`, `biSup_finset`, `bot`, `finset_sup`, `iSup`, `pi`, `prod`, `sup`, `fg_iff`, `fg_iff_addSubmonoid_fg`, `fg_iff_mul_fg`, `biSup`, `biSup_finset`, `bot`, `exists_minimal_closure_eq`, `finset_sup`, `iSup`, `map`, `map_injective`, `pi`, `prod`, `sum`, `sup`, `exists_minimal_closure_eq_top`, `fg_eqLocusM`, `fg_iff`, `fg_iff_mul_fg`, `fg_of_subtractive`, `iSup_map_single`, `multiples_fg`, `fg_of_wellQuasiOrderedLE`, `out`, `closure_finite_fg`, `closure_finset_fg`, `fg_def`, `fg_iff`, `fg_iff'`, `fg_iff_exists_freeGroup_hom_surjective`, `fg_iff_monoid_fg`, `fg_iff_subgroup_fg`, `fg_of_finite`, `fg_of_mul_group_fg`, `fg_of_surjective`, `fg_range`, `iff_add_fg`, `fg_top`, `closure_finite_fg`, `closure_finset_fg`, `fg_def`, `fg_iff`, `fg_iff_add_fg`, `fg_iff_exists_freeMonoid_hom_surjective`, `fg_iff_submonoid_fg`, `fg_of_addMonoid_fg`, `fg_of_finite`, `fg_of_group_fg`, `fg_of_surjective`, `fg_range`, `powers_fg`, `instAddGroupFG`, `instAddMonoidFG`, `instGroupFG`, `instMonoidFG`, `instAddGroupFG`, `instAddMonoidFG`, `instGroupFG`, `instMonoidFG`, `fg`, `fg`, `biSup`, `biSup_finset`, `bot`, `finset_sup`, `iSup`, `pi`, `prod`, `sup`, `fg_iff`, `fg_iff_add_fg`, `fg_iff_submonoid_fg`, `biSup`, `biSup_finset`, `bot`, `exists_minimal_closure_eq`, `finset_sup`, `iSup`, `map`, `map_injective`, `pi`, `prod`, `sup`, `exists_minimal_closure_eq_top`, `fg_eqLocusM`, `fg_iff`, `fg_iff_add_fg`, `fg_of_divisive`, `iSup_map_mulSingle`, `powers_fg`	130
Total	130

AddCommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_wellQuasiOrderedLE` 📖	mathematical	—	`AddMonoid.FG` `toAddMonoid`	—	`AddSubmonoid.fg_of_subtractive` `AddSubmonoid.mem_top`

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_finite_fg` 📖	mathematical	—	`FG` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.closure` `AddSubgroup.toAddGroup`	—	`closure_finset_fg` `Set.coe_toFinset`
`closure_finset_fg` 📖	mathematical	—	`FG` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `AddSubgroup.toAddGroup`	—	`Function.Injective.injOn` `Subtype.coe_injective` `Finset.coe_preimage` `AddSubgroup.coe_subtype` `AddSubgroup.closure_preimage_eq_top`
`fg_def` 📖	mathematical	—	`FG` `AddSubgroup.FG` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`FG.out`
`fg_iff` 📖	mathematical	—	`FG` `AddSubgroup.closure` `Top.top` `AddSubgroup` `AddSubgroup.instTop` `Set.Finite`	—	`AddSubgroup.fg_iff` `FG.out`
`fg_iff'` 📖	mathematical	—	`FG` `Finset.card` `AddSubgroup.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`fg_def`
`fg_iff_addMonoid_fg` 📖	mathematical	—	`FG` `AddMonoid.FG` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`AddMonoid.fg_def` `AddSubgroup.fg_iff_addSubmonoid_fg` `fg_def`
`fg_iff_addSubgroup_fg` 📖	mathematical	—	`FG` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.FG`	—	`fg_iff_addMonoid_fg` `AddMonoid.fg_iff_addSubmonoid_fg` `AddSubgroup.fg_iff_addSubmonoid_fg`
`fg_iff_exists_freeAddGroup_hom_surjective` 📖	mathematical	—	`FG` `FreeAddGroup` `Set.Elem` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `FreeAddGroup.instAddGroup` `AddMonoidHom.instFunLike`	—	`Finset.finite_toSet` `AddMonoidHom.range_eq_top` `FreeAddGroup.closure_eq_range` `fg_iff` `AddMonoidHom.map_closure` `FreeAddGroup.closure_range_of` `AddMonoidHom.range_eq_map` `AddMonoidHom.range_eq_top_of_surjective` `Set.toFinite` `Finite.Set.finite_image` `Finite.Set.finite_range`
`fg_iff_mul_fg` 📖	mathematical	—	`FG` `Group.FG` `Multiplicative` `Multiplicative.group`	—	`AddSubgroup.fg_iff_mul_fg` `FG.out` `Group.FG.out`
`fg_of_finite` 📖	mathematical	—	`FG`	—	`nonempty_fintype` `Finset.coe_univ` `AddSubgroup.closure_univ`
`fg_of_group_fg` 📖	mathematical	—	`FG` `Additive` `Additive.addGroup`	—	`GroupFG.iff_add_fg`
`fg_of_surjective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `AddMonoidHom.instFunLike`	`FG`	—	`fg_iff_addMonoid_fg` `AddMonoid.fg_of_surjective`
`fg_range` 📖	mathematical	—	`FG` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.range` `AddSubgroup.toAddGroup`	—	`fg_of_surjective` `AddMonoidHom.rangeRestrict_surjective`
`instFGInt` 📖	mathematical	—	`FG` `Int.instAddGroup`	—	`Finset.coe_singleton` `Int.addSubgroupClosure_one`

AddGroup.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`AddSubgroup.FG` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	—

AddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_finite_fg` 📖	mathematical	—	`FG` `AddSubmonoid` `toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `AddSubmonoid.toAddMonoid`	—	`closure_finset_fg` `Set.coe_toFinset`
`closure_finset_fg` 📖	mathematical	—	`FG` `AddSubmonoid` `toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `AddSubmonoid.toAddMonoid`	—	`Function.Injective.injOn` `Subtype.coe_injective` `Finset.coe_preimage` `AddSubmonoid.closure_closure_coe_preimage`
`fG_iff` 📖	mathematical	—	`FG` `AddSubmonoid.FG` `Top.top` `AddSubmonoid` `toAddZeroClass` `AddSubmonoid.instTop`	—	—
`fg_def` 📖	mathematical	—	`FG` `AddSubmonoid.FG` `Top.top` `AddSubmonoid` `toAddZeroClass` `AddSubmonoid.instTop`	—	`FG.fg_top`
`fg_iff` 📖	mathematical	—	`FG` `AddSubmonoid.closure` `toAddZeroClass` `Top.top` `AddSubmonoid` `AddSubmonoid.instTop` `Set.Finite`	—	`AddSubmonoid.fg_iff` `FG.fg_top`
`fg_iff_addSubmonoid_fg` 📖	mathematical	—	`FG` `AddSubmonoid` `toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.toAddMonoid` `AddSubmonoid.FG`	—	`AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.mrange_subtype` `AddMonoidHom.mrange_eq_map` `AddSubmonoid.FG.map` `FG.fg_top` `AddSubmonoid.FG.map_injective` `Subtype.coe_injective`
`fg_iff_exists_freeAddMonoid_hom_surjective` 📖	mathematical	—	`FG` `FreeAddMonoid` `Set.Elem` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `FreeAddMonoid.instAddCancelMonoid` `AddMonoidHom.instFunLike`	—	`Finset.finite_toSet` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.mrange_eq_top` `AddSubmonoid.closure_eq_mrange` `fg_iff` `AddMonoidHom.map_mclosure` `AddSubmonoid.map.congr_simp` `FreeAddMonoid.closure_range_of` `AddMonoidHom.mrange_eq_map` `AddMonoidHom.mrange_eq_top_of_surjective` `Set.toFinite` `Finite.Set.finite_image` `Finite.Set.finite_range`
`fg_iff_mul_fg` 📖	mathematical	—	`FG` `Monoid.FG` `Multiplicative` `Multiplicative.monoid`	—	`AddSubmonoid.fg_iff_mul_fg` `FG.fg_top` `Monoid.FG.fg_top`
`fg_of_addGroup_fg` 📖	mathematical	—	`FG` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`AddGroup.fg_iff_addMonoid_fg`
`fg_of_finite` 📖	mathematical	—	`FG`	—	`nonempty_fintype` `Finset.coe_univ` `AddSubmonoid.closure_univ`
`fg_of_monoid_fg` 📖	mathematical	—	`FG` `Additive` `Additive.addMonoid`	—	`Monoid.fg_iff_add_fg`
`fg_of_surjective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `toAddZeroClass` `AddMonoidHom.instFunLike`	`FG`	—	`fg_def` `Finset.coe_image` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.map_mclosure` `AddMonoidHom.mrange_eq_map` `AddMonoidHom.mrange_eq_top`
`fg_range` 📖	mathematical	—	`FG` `AddSubmonoid` `toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddMonoidHom.mrange` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.toAddMonoid`	—	`fg_of_surjective` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.mrangeRestrict_surjective`
`instFGNat` 📖	mathematical	—	`FG` `Nat.instAddMonoid`	—	`Finset.coe_singleton` `Nat.addSubmonoidClosure_one`
`multiples_fg` 📖	mathematical	—	`FG` `AddSubmonoid` `toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.multiples` `AddSubmonoid.toAddMonoid`	—	`fg_iff_addSubmonoid_fg` `AddSubmonoid.multiples_fg`

AddMonoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_top` 📖	mathematical	—	`AddSubmonoid.FG` `Top.top` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instTop`	—	—

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_iff` 📖	mathematical	—	`FG` `closure` `Set.Finite`	—	`Finset.finite_toSet` `Set.Finite.coe_toFinset`
`fg_iff_addSubmonoid_fg` 📖	mathematical	—	`FG` `AddSubmonoid.FG` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSubmonoid`	—	`AddSubmonoid.fg_iff` `closure_toAddSubmonoid` `Set.Finite.union` `Finset.finite_toSet` `Set.Finite.neg` `le_antisymm` `closure_le` `coe_toAddSubmonoid` `AddSubmonoid.subset_closure` `toAddSubmonoid_le` `AddSubmonoid.closure_le` `subset_closure`
`fg_iff_mul_fg` 📖	mathematical	—	`FG` `Subgroup.FG` `Multiplicative` `Multiplicative.group` `DFunLike.coe` `OrderIso` `AddSubgroup` `Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Subgroup.instPartialOrder` `instFunLikeOrderIso` `toSubgroup`	—	`fg_iff_addSubmonoid_fg` `Subgroup.fg_iff_submonoid_fg` `AddSubmonoid.fg_iff_mul_fg`

AddSubgroup.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biSup` 📖	mathematical	`AddSubgroup.FG`	`iSup` `AddSubgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice` `Set` `Set.instMembership`	—	`iSup_congr_Prop` `Set.Finite.mem_toFinset` `biSup_finset`
`biSup_finset` 📖	mathematical	`AddSubgroup.FG`	`iSup` `AddSubgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice` `Finset` `Finset.instMembership`	—	`Finset.sup_eq_iSup` `finset_sup`
`bot` 📖	mathematical	—	`AddSubgroup.FG` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`Finset.coe_empty` `AddSubgroup.closure_empty`
`finset_sup` 📖	mathematical	`AddSubgroup.FG`	`Finset.sup` `AddSubgroup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	—	`Finset.sup_induction` `bot` `sup`
`iSup` 📖	mathematical	`AddSubgroup.FG`	`iSup` `AddSubgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice`	—	`iSup_congr_Prop` `Set.mem_univ` `iSup_pos` `iSup_plift_down` `biSup` `Set.finite_univ` `instFinitePLift`
`pi` 📖	mathematical	`AddSubgroup.FG`	`Pi.addGroup` `AddSubgroup.pi` `Set.univ`	—	`AddSubgroup.fg_iff_addSubmonoid_fg` `AddSubmonoid.FG.pi`
`prod` 📖	mathematical	`AddSubgroup.FG`	`Prod.instAddGroup` `AddSubgroup.prod`	—	`AddSubgroup.fg_iff_addSubmonoid_fg` `AddSubmonoid.FG.prod`
`sup` 📖	mathematical	`AddSubgroup.FG`	`AddSubgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AddSubgroup.instCompleteLattice`	—	`Finset.coe_union` `AddSubgroup.closure_union`

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_minimal_closure_eq_top` 📖	mathematical	—	`Minimal` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `AddSubmonoid` `AddMonoid.toAddZeroClass` `closure` `SetLike.coe` `Finset.instSetLike` `Top.top` `instTop`	—	`FG.exists_minimal_closure_eq` `AddMonoid.FG.fg_top`
`fg_eqLocusM` 📖	mathematical	—	`FG` `AddCommMonoid.toAddMonoid` `AddMonoidHom.eqLocusM` `AddMonoid.toAddZeroClass`	—	`fg_of_subtractive` `AddMonoidHom.mem_eqLocusM` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `IsCancelAdd.toIsLeftCancelAdd`
`fg_iff` 📖	mathematical	—	`FG` `closure` `AddMonoid.toAddZeroClass` `Set.Finite`	—	`Finset.finite_toSet` `Set.Finite.coe_toFinset`
`fg_iff_mul_fg` 📖	mathematical	—	`FG` `Submonoid.FG` `Multiplicative` `Multiplicative.monoid` `DFunLike.coe` `OrderIso` `AddSubmonoid` `AddMonoid.toAddZeroClass` `Submonoid` `Multiplicative.mulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submonoid.instPartialOrder` `instFunLikeOrderIso` `toSubmonoid`	—	`Submonoid.fg_iff_add_fg`
`fg_of_subtractive` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike`	`FG`	—	`Set.isPWO_of_wellQuasiOrderedLE` `fg_iff` `ext` `closure_eq` `closure_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `setOf_minimal_subset` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `instAddSubmonoidClass` `Set.WellFoundedOn.induction` `Set.PartiallyWellOrderedOn.wellFoundedOn` `instIsPreorderLe` `mem_closure_of_mem` `exists_lt_of_not_minimal` `ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `LT.lt.le` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `LT.lt.not_ge` `LT.lt.ne` `pos_of_lt_add_right` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `le_add_self` `add_le_iff_nonpos_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_swap_add_of_contravariant_add` `pos_of_ne_zero` `IsAntichain.finite_of_partiallyWellOrderedOn` `setOf_minimal_antichain` `Set.IsPWO.mono`
`iSup_map_single` 📖	mathematical	—	`iSup` `AddSubmonoid` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `map` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.single` `pi` `Set.univ`	—	`LE.le.antisymm` `AddMonoidHom.instAddMonoidHomClass` `iSup_map_single_le` `Pi.single_apply_addCommute` `Finset.noncommSum_single` `noncommSum_mem` `mem_iSup_of_mem` `mem_map_of_mem`
`multiples_fg` 📖	mathematical	—	`FG` `multiples`	—	`multiples_eq_closure` `Finset.coe_singleton`

AddSubmonoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biSup` 📖	mathematical	`AddSubmonoid.FG`	`iSup` `AddSubmonoid` `AddMonoid.toAddZeroClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice` `Set` `Set.instMembership`	—	`iSup_congr_Prop` `Set.Finite.mem_toFinset` `biSup_finset`
`biSup_finset` 📖	mathematical	`AddSubmonoid.FG`	`iSup` `AddSubmonoid` `AddMonoid.toAddZeroClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice` `Finset` `Finset.instMembership`	—	`Finset.sup_eq_iSup` `finset_sup`
`bot` 📖	mathematical	—	`AddSubmonoid.FG` `Bot.bot` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instBot`	—	`Finset.coe_empty` `AddSubmonoid.closure_empty`
`exists_minimal_closure_eq` 📖	mathematical	`AddSubmonoid.FG`	`Minimal` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.closure` `SetLike.coe` `Finset.instSetLike`	—	`exists_minimal_of_wellFoundedLT` `Finset.wellFoundedLT`
`finset_sup` 📖	mathematical	`AddSubmonoid.FG`	`Finset.sup` `AddSubmonoid` `AddMonoid.toAddZeroClass` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	—	`Finset.sup_induction` `bot` `sup`
`iSup` 📖	mathematical	`AddSubmonoid.FG`	`iSup` `AddSubmonoid` `AddMonoid.toAddZeroClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice`	—	`iSup_congr_Prop` `Set.mem_univ` `iSup_pos` `iSup_plift_down` `biSup` `Set.finite_univ` `instFinitePLift`
`map` 📖	mathematical	`AddSubmonoid.FG`	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass`	—	`AddMonoidHom.instAddMonoidHomClass` `Finset.coe_image` `AddMonoidHom.map_mclosure`
`map_injective` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid.FG` `AddSubmonoid.map` `AddMonoidHom.instAddMonoidHomClass`	—	—	`AddMonoidHom.instAddMonoidHomClass` `Function.Injective.injOn` `AddSubmonoid.map_injective_of_injective` `AddMonoidHom.map_mclosure` `Finset.coe_preimage` `Set.image_preimage_eq_iff` `AddMonoidHom.coe_mrange` `AddSubmonoid.closure_le` `AddMonoidHom.mrange_eq_map` `AddSubmonoid.monotone_map` `le_top`
`pi` 📖	mathematical	`AddSubmonoid.FG`	`Pi.addMonoid` `AddSubmonoid.pi` `AddMonoid.toAddZeroClass` `Set.univ`	—	`Finset.coe_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_univ` `Set.biUnion_univ` `AddSubmonoid.closure_iUnion` `Finset.coe_image` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.map_mclosure` `AddSubmonoid.map.congr_simp` `AddSubmonoid.iSup_map_single`
`prod` 📖	mathematical	`AddSubmonoid.FG`	`Prod.instAddMonoid` `AddSubmonoid.prod` `AddMonoid.toAddZeroClass`	—	`Finset.coe_union` `Finset.coe_product` `Finset.coe_singleton` `AddSubmonoid.closure_union` `AddSubmonoid.closure_prod_zero` `AddSubmonoid.closure_zero_prod` `AddSubmonoid.prod_bot_sup_bot_prod`
`sum` 📖	mathematical	`AddSubmonoid.FG`	`Prod.instAddMonoid` `AddSubmonoid.prod` `AddMonoid.toAddZeroClass`	—	`prod`
`sup` 📖	mathematical	`AddSubmonoid.FG`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice`	—	`Finset.coe_union` `AddSubmonoid.closure_union`

CommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_wellQuasiOrderedLE` 📖	mathematical	—	`Monoid.FG` `toMonoid`	—	`Submonoid.fg_of_divisive`

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_finite_fg` 📖	mathematical	—	`FG` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.closure` `Subgroup.toGroup`	—	`closure_finset_fg` `Set.coe_toFinset`
`closure_finset_fg` 📖	mathematical	—	`FG` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Subgroup.toGroup`	—	`Function.Injective.injOn` `Subtype.coe_injective` `Finset.coe_preimage` `Subgroup.coe_subtype` `Subgroup.closure_preimage_eq_top`
`fg_def` 📖	mathematical	—	`FG` `Subgroup.FG` `Top.top` `Subgroup` `Subgroup.instTop`	—	`FG.out`
`fg_iff` 📖	mathematical	—	`FG` `Subgroup.closure` `Top.top` `Subgroup` `Subgroup.instTop` `Set.Finite`	—	`Subgroup.fg_iff` `FG.out`
`fg_iff'` 📖	mathematical	—	`FG` `Finset.card` `Subgroup.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Subgroup` `Subgroup.instTop`	—	`fg_def`
`fg_iff_exists_freeGroup_hom_surjective` 📖	mathematical	—	`FG` `FreeGroup` `Set.Elem` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `FreeGroup.instGroup` `MonoidHom.instFunLike`	—	`Finset.finite_toSet` `MonoidHom.range_eq_top` `FreeGroup.closure_eq_range` `fg_iff` `FreeGroup.closure_range_of` `MonoidHom.range_eq_top_of_surjective` `Set.toFinite` `Finite.Set.finite_image` `Finite.Set.finite_range`
`fg_iff_monoid_fg` 📖	mathematical	—	`FG` `Monoid.FG` `DivInvMonoid.toMonoid` `toDivInvMonoid`	—	`Monoid.fg_def` `Subgroup.fg_iff_submonoid_fg` `fg_def`
`fg_iff_subgroup_fg` 📖	mathematical	—	`FG` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.FG`	—	`fg_iff_monoid_fg` `Monoid.fg_iff_submonoid_fg` `Subgroup.fg_iff_submonoid_fg`
`fg_of_finite` 📖	mathematical	—	`FG`	—	`nonempty_fintype` `Finset.coe_univ` `Subgroup.closure_univ`
`fg_of_mul_group_fg` 📖	mathematical	—	`FG` `Multiplicative` `Multiplicative.group`	—	`AddGroup.fg_iff_mul_fg`
`fg_of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `MonoidHom.instFunLike`	`FG`	—	`fg_iff_monoid_fg` `Monoid.fg_of_surjective`
`fg_range` 📖	mathematical	—	`FG` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `Subgroup.toGroup`	—	`fg_of_surjective` `MonoidHom.rangeRestrict_surjective`

Group.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`Subgroup.FG` `Top.top` `Subgroup` `Subgroup.instTop`	—	—

GroupFG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_add_fg` 📖	mathematical	—	`Group.FG` `AddGroup.FG` `Additive` `Additive.addGroup`	—	`Subgroup.fg_iff_add_fg` `Group.FG.out` `AddGroup.FG.out`

Monoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_finite_fg` 📖	mathematical	—	`FG` `Submonoid` `toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.closure` `Submonoid.toMonoid`	—	`closure_finset_fg` `Set.coe_toFinset`
`closure_finset_fg` 📖	mathematical	—	`FG` `Submonoid` `toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `Submonoid.toMonoid`	—	`Function.Injective.injOn` `Subtype.coe_injective` `Finset.coe_preimage` `Submonoid.closure_closure_coe_preimage`
`fg_def` 📖	mathematical	—	`FG` `Submonoid.FG` `Top.top` `Submonoid` `toMulOneClass` `Submonoid.instTop`	—	`FG.fg_top`
`fg_iff` 📖	mathematical	—	`FG` `Submonoid.closure` `toMulOneClass` `Top.top` `Submonoid` `Submonoid.instTop` `Set.Finite`	—	`Submonoid.fg_iff` `FG.fg_top`
`fg_iff_add_fg` 📖	mathematical	—	`FG` `AddMonoid.FG` `Additive` `Additive.addMonoid`	—	`Submonoid.fg_iff_add_fg` `FG.fg_top` `AddMonoid.FG.fg_top`
`fg_iff_exists_freeMonoid_hom_surjective` 📖	mathematical	—	`FG` `FreeMonoid` `Set.Elem` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MonoidHom.instFunLike`	—	`Finset.finite_toSet` `MonoidHom.instMonoidHomClass` `MonoidHom.mrange_eq_top` `Submonoid.closure_eq_mrange` `fg_iff` `Submonoid.map.congr_simp` `FreeMonoid.closure_range_of` `MonoidHom.mrange_eq_top_of_surjective` `Set.toFinite` `Finite.Set.finite_image` `Finite.Set.finite_range`
`fg_iff_submonoid_fg` 📖	mathematical	—	`FG` `Submonoid` `toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.toMonoid` `Submonoid.FG`	—	`MonoidHom.instMonoidHomClass` `Submonoid.mrange_subtype` `MonoidHom.mrange_eq_map` `Submonoid.FG.map` `FG.fg_top` `Submonoid.FG.map_injective` `Subtype.coe_injective`
`fg_of_addMonoid_fg` 📖	mathematical	—	`FG` `Multiplicative` `Multiplicative.monoid`	—	`AddMonoid.fg_iff_mul_fg`
`fg_of_finite` 📖	mathematical	—	`FG`	—	`nonempty_fintype` `Finset.coe_univ` `Submonoid.closure_univ`
`fg_of_group_fg` 📖	mathematical	—	`FG` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Group.fg_iff_monoid_fg`
`fg_of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `toMulOneClass` `MonoidHom.instFunLike`	`FG`	—	`fg_def` `Finset.coe_image` `MonoidHom.instMonoidHomClass` `MonoidHom.map_mclosure` `MonoidHom.mrange_eq_map` `MonoidHom.mrange_eq_top`
`fg_range` 📖	mathematical	—	`FG` `Submonoid` `toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `MonoidHom.mrange` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `Submonoid.toMonoid`	—	`fg_of_surjective` `MonoidHom.instMonoidHomClass` `MonoidHom.mrangeRestrict_surjective`
`powers_fg` 📖	mathematical	—	`FG` `Submonoid` `toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers` `Submonoid.toMonoid`	—	`fg_iff_submonoid_fg` `Submonoid.powers_fg`

Monoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_top` 📖	mathematical	—	`Submonoid.FG` `Top.top` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instTop`	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddGroupFG` 📖	mathematical	`AddGroup.FG`	`addGroup`	—	`AddSubgroup.pi_top` `AddSubgroup.FG.pi` `AddGroup.FG.out`
`instAddMonoidFG` 📖	mathematical	`AddMonoid.FG`	`addMonoid`	—	`AddSubmonoid.pi_top` `AddSubmonoid.FG.pi` `AddMonoid.FG.fg_top`
`instGroupFG` 📖	mathematical	`Group.FG`	`group`	—	`Subgroup.pi_top` `Subgroup.FG.pi` `Group.FG.out`
`instMonoidFG` 📖	mathematical	`Monoid.FG`	`monoid`	—	`Submonoid.pi_top` `Submonoid.FG.pi` `Monoid.FG.fg_top`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddGroupFG` 📖	mathematical	—	`AddGroup.FG` `instAddGroup`	—	`AddSubgroup.top_prod_top` `AddSubgroup.FG.prod` `AddGroup.FG.out`
`instAddMonoidFG` 📖	mathematical	—	`AddMonoid.FG` `instAddMonoid`	—	`AddSubmonoid.top_prod_top` `AddSubmonoid.FG.prod` `AddMonoid.FG.fg_top`
`instGroupFG` 📖	mathematical	—	`Group.FG` `instGroup`	—	`Subgroup.top_prod_top` `Subgroup.FG.prod` `Group.FG.out`
`instMonoidFG` 📖	mathematical	—	`Monoid.FG` `instMonoid`	—	`Submonoid.top_prod_top` `Submonoid.FG.prod` `Monoid.FG.fg_top`

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg` 📖	mathematical	—	`AddGroup.FG` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	`AddGroup.fg_of_surjective` `mk'_surjective`

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg` 📖	mathematical	—	`Group.FG` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	`Group.fg_of_surjective` `mk'_surjective`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_iff` 📖	mathematical	—	`FG` `closure` `Set.Finite`	—	`Finset.finite_toSet` `Set.Finite.coe_toFinset`
`fg_iff_add_fg` 📖	mathematical	—	`FG` `AddSubgroup.FG` `Additive` `Additive.addGroup` `DFunLike.coe` `OrderIso` `Subgroup` `AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AddSubgroup.instPartialOrder` `instFunLikeOrderIso` `toAddSubgroup`	—	`fg_iff_submonoid_fg` `AddSubgroup.fg_iff_addSubmonoid_fg` `Submonoid.fg_iff_add_fg`
`fg_iff_submonoid_fg` 📖	mathematical	—	`FG` `Submonoid.FG` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSubmonoid`	—	`Submonoid.fg_iff` `closure_toSubmonoid` `Set.Finite.union` `Finset.finite_toSet` `Set.Finite.inv` `le_antisymm` `closure_le` `coe_toSubmonoid` `Submonoid.subset_closure` `toSubmonoid_le` `Submonoid.closure_le` `subset_closure`

Subgroup.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biSup` 📖	mathematical	`Subgroup.FG`	`iSup` `Subgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice` `Set` `Set.instMembership`	—	`iSup_congr_Prop` `biSup_finset`
`biSup_finset` 📖	mathematical	`Subgroup.FG`	`iSup` `Subgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice` `Finset` `Finset.instMembership`	—	`Finset.sup_eq_iSup` `finset_sup`
`bot` 📖	mathematical	—	`Subgroup.FG` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`Finset.coe_empty` `Subgroup.closure_empty`
`finset_sup` 📖	mathematical	`Subgroup.FG`	`Finset.sup` `Subgroup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	—	`Finset.sup_induction` `bot` `sup`
`iSup` 📖	mathematical	`Subgroup.FG`	`iSup` `Subgroup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`iSup_congr_Prop` `iSup_pos` `iSup_plift_down` `biSup` `Set.finite_univ` `instFinitePLift`
`pi` 📖	mathematical	`Subgroup.FG`	`Pi.group` `Subgroup.pi` `Set.univ`	—	`Submonoid.FG.pi`
`prod` 📖	mathematical	`Subgroup.FG`	`Prod.instGroup` `Subgroup.prod`	—	`Subgroup.fg_iff_submonoid_fg` `Submonoid.FG.prod`
`sup` 📖	mathematical	`Subgroup.FG`	`Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`Finset.coe_union` `Subgroup.closure_union`

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_minimal_closure_eq_top` 📖	mathematical	—	`Minimal` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `Submonoid` `Monoid.toMulOneClass` `closure` `SetLike.coe` `Finset.instSetLike` `Top.top` `instTop`	—	`FG.exists_minimal_closure_eq` `Monoid.FG.fg_top`
`fg_eqLocusM` 📖	mathematical	—	`FG` `CommMonoid.toMonoid` `MonoidHom.eqLocusM` `Monoid.toMulOneClass`	—	`fg_of_divisive` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `IsCancelMul.toIsLeftCancelMul`
`fg_iff` 📖	mathematical	—	`FG` `closure` `Monoid.toMulOneClass` `Set.Finite`	—	`Finset.finite_toSet` `Set.Finite.coe_toFinset`
`fg_iff_add_fg` 📖	mathematical	—	`FG` `AddSubmonoid.FG` `Additive` `Additive.addMonoid` `DFunLike.coe` `OrderIso` `Submonoid` `Monoid.toMulOneClass` `AddSubmonoid` `Additive.addZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AddSubmonoid.instPartialOrder` `instFunLikeOrderIso` `toAddSubmonoid`	—	`fg_iff` `AddSubmonoid.fg_iff` `OrderIso.symm_apply_apply`
`fg_of_divisive` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike`	`FG`	—	`Set.isPWO_of_wellQuasiOrderedLE` `fg_iff` `ext` `closure_eq` `closure_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `setOf_minimal_subset` `SubmonoidClass.toOneMemClass` `instSubmonoidClass` `Set.WellFoundedOn.induction` `Set.PartiallyWellOrderedOn.wellFoundedOn` `instIsPreorderLe` `mem_closure_of_mem` `exists_lt_of_not_minimal` `ExistsMulOfLE.exists_mul_of_le` `CanonicallyOrderedMul.toExistsMulOfLE` `LT.lt.le` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `LT.lt.not_ge` `LT.lt.ne` `one_lt_of_lt_mul_right` `IsOrderedCancelMonoid.toMulLeftReflectLT` `le_mul_self` `mul_le_iff_le_one_left'` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT` `IsCancelMul.toIsRightCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `contravariant_swap_mul_of_contravariant_mul` `one_lt_of_ne_one` `IsAntichain.finite_of_partiallyWellOrderedOn` `setOf_minimal_antichain` `Set.IsPWO.mono`
`iSup_map_mulSingle` 📖	mathematical	—	`iSup` `Submonoid` `Pi.mulOneClass` `Monoid.toMulOneClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `map` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MonoidHom.mulSingle` `pi` `Set.univ`	—	`LE.le.antisymm` `MonoidHom.instMonoidHomClass` `iSup_map_mulSingle_le` `Pi.mulSingle_apply_commute` `Finset.noncommProd_mulSingle` `noncommProd_mem` `mem_iSup_of_mem` `mem_map_of_mem`
`powers_fg` 📖	mathematical	—	`FG` `powers`	—	`powers_eq_closure` `Finset.coe_singleton`

Submonoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biSup` 📖	mathematical	`Submonoid.FG`	`iSup` `Submonoid` `Monoid.toMulOneClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice` `Set` `Set.instMembership`	—	`iSup_congr_Prop` `biSup_finset`
`biSup_finset` 📖	mathematical	`Submonoid.FG`	`iSup` `Submonoid` `Monoid.toMulOneClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice` `Finset` `Finset.instMembership`	—	`Finset.sup_eq_iSup` `finset_sup`
`bot` 📖	mathematical	—	`Submonoid.FG` `Bot.bot` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instBot`	—	`Finset.coe_empty` `Submonoid.closure_empty`
`exists_minimal_closure_eq` 📖	mathematical	`Submonoid.FG`	`Minimal` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `Submonoid` `Monoid.toMulOneClass` `Submonoid.closure` `SetLike.coe` `Finset.instSetLike`	—	`exists_minimal_of_wellFoundedLT` `Finset.wellFoundedLT`
`finset_sup` 📖	mathematical	`Submonoid.FG`	`Finset.sup` `Submonoid` `Monoid.toMulOneClass` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	—	`Finset.sup_induction` `bot` `sup`
`iSup` 📖	mathematical	`Submonoid.FG`	`iSup` `Submonoid` `Monoid.toMulOneClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice`	—	`iSup_congr_Prop` `iSup_pos` `iSup_plift_down` `biSup` `Set.finite_univ` `instFinitePLift`
`map` 📖	mathematical	`Submonoid.FG`	`Submonoid.map` `Monoid.toMulOneClass` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass`	—	`MonoidHom.instMonoidHomClass` `Finset.coe_image` `MonoidHom.map_mclosure`
`map_injective` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid.FG` `Submonoid.map` `MonoidHom.instMonoidHomClass`	—	—	`MonoidHom.instMonoidHomClass` `Function.Injective.injOn` `Submonoid.map_injective_of_injective` `MonoidHom.map_mclosure` `Finset.coe_preimage` `Set.image_preimage_eq_iff` `MonoidHom.coe_mrange` `Submonoid.closure_le` `MonoidHom.mrange_eq_map` `Submonoid.monotone_map` `le_top`
`pi` 📖	mathematical	`Submonoid.FG`	`Pi.monoid` `Submonoid.pi` `Monoid.toMulOneClass` `Set.univ`	—	`Finset.coe_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_univ` `Set.biUnion_univ` `Submonoid.closure_iUnion` `Finset.coe_image` `MonoidHom.instMonoidHomClass` `Submonoid.map.congr_simp` `Submonoid.iSup_map_mulSingle`
`prod` 📖	mathematical	`Submonoid.FG`	`Prod.instMonoid` `Submonoid.prod` `Monoid.toMulOneClass`	—	`Finset.coe_union` `Finset.coe_product` `Finset.coe_singleton` `Submonoid.closure_union` `Submonoid.closure_prod_one` `Submonoid.closure_one_prod` `Submonoid.prod_bot_sup_bot_prod`
`sup` 📖	mathematical	`Submonoid.FG`	`Submonoid` `Monoid.toMulOneClass` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submonoid.instCompleteLattice`	—	`Finset.coe_union` `Submonoid.closure_union`

---

← Back to Index