Basic

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

Statistics

Metric	Count
Definitions ofClosureMEqTopLeft, ofClosureMEqTopRight, closure, gi, instCompleteLattice, instInfSet, addSubmonoid, submonoid, ofClosureMEqTopLeft, ofClosureMEqTopRight, closure, gi, instCompleteLattice, instInfSet	14
Theorems coe_ofClosureMEqTopLeft, coe_ofClosureMEqTopRight, eqOn_closureM, eq_of_eqOn_denseM, closure_empty, closure_eq, closure_eq_of_le, closure_iUnion, closure_induction, closure_induction₂, closure_insert_zero, closure_le, closure_mono, closure_sdiff_eq_closure, closure_sdiff_singleton_zero, closure_singleton_le_iff_mem, closure_union, closure_univ, coe_iInf, coe_sInf, dense_induction, disjoint_def, disjoint_def', iSup_eq_closure, mem_closure, mem_closure_of_mem, mem_iInf, mem_iSup, mem_sInf, notMem_of_notMem_closure, subset_closure, sup_eq_closure, mem_addSubmonoid_iff, mem_submonoid_iff, coe_ofClosureMEqTopLeft, coe_ofClosureMEqTopRight, eqOn_closureM, eq_of_eqOn_denseM, closure_empty, closure_eq, closure_eq_of_le, closure_eq_one_union, closure_iUnion, closure_induction, closure_induction₂, closure_insert_one, closure_le, closure_mono, closure_sdiff_eq_closure, closure_sdiff_singleton_one, closure_singleton_le_iff_mem, closure_union, closure_univ, coe_iInf, coe_sInf, dense_induction, disjoint_def, disjoint_def', iSup_eq_closure, mem_closure, mem_closure_of_mem, mem_iInf, mem_iSup, mem_sInf, notMem_of_notMem_closure, subset_closure, sup_eq_closure	67
Total	81

AddMonoidHom

Definitions

Name	Category	Theorems
ofClosureMEqTopLeft 📖	CompOp	1 math math: coe_ofClosureMEqTopLeft
ofClosureMEqTopRight 📖	CompOp	1 math math: coe_ofClosureMEqTopRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofClosureMEqTopLeft 📖	mathematical	AddSubmonoid.closure AddMonoid.toAddZeroClass Top.top AddSubmonoid AddSubmonoid.instTop AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	DFunLike.coe AddMonoidHom instFunLike ofClosureMEqTopLeft	—	—
coe_ofClosureMEqTopRight 📖	mathematical	AddSubmonoid.closure AddMonoid.toAddZeroClass Top.top AddSubmonoid AddSubmonoid.instTop AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	DFunLike.coe AddMonoidHom instFunLike ofClosureMEqTopRight	—	—
eqOn_closureM 📖	mathematical	Set.EqOn DFunLike.coe AddMonoidHom AddZeroClass.toAddZero instFunLike	SetLike.coe AddSubmonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	AddSubmonoid.closure_le
eq_of_eqOn_denseM 📖	—	AddSubmonoid.closure Top.top AddSubmonoid AddSubmonoid.instTop Set.EqOn DFunLike.coe AddMonoidHom AddZeroClass.toAddZero instFunLike	—	—	eq_of_eqOn_topM eqOn_closureM

AddSubmonoid

Definitions

Name	Category	Theorems
closure 📖	CompOp	134 math math: AddCommute.exists_addOrderOf_eq_lcm, Ideal.Filtration.submodule_closure_single, Submodule.span_nat_eq_addSubmonoid_closure, Submonoid.subsemiringClosure_toAddSubmonoid, add_subset_closure, Subsemiring.closure_addSubmonoid_closure, sup_eq_closure, IsLinearSet.closure_finset, multiples_eq_closure, mem_closure_finset, AddMonoid.closure_finite_fg, AddMonoid.fg_iff, frobeniusNumber_iff, closure_addIrreducible, closure_nsmul, IsSemilinearSet.closure_finset, Set.IsPWO.addSubmonoid_closure, Nat.exists_mem_closure_of_ge, closure_sdiff_singleton_zero, mem_closure_range_iff, Submonoid.subsemiringClosure_coe, Submodule.closure_le_toAddSubmonoid_span, StarOrderedRing.lt_iff, isLinearSet_iff, closure_le_centralizer_centralizer, closure_prod, closure_pi, closure_image_isAddIndecomposable_baseOf, StarOrderedRing.pos_iff, closure_univ, Nat.addSubmonoidClosure_one, Submonoid.toAddSubmonoid_closure, toNatSubmodule_closure, NonUnitalSubsemiring.closure_addSubmonoid_closure, IsLinearSet.closure_of_finite, closure_union, closure_isSquare, mem_closure_iff_exists_finset_subset, AddMonoidHom.mclosure_preimage_le, subset_closure, AddMonoidHom.map_mclosure, closure_singleton_eq, closure_zero_prod, toSubmonoid_closure, AddMonoid.closure_finset_fg, HahnSeries.SummableFamily.support_pow_subset_closure, exists_minimal_closure_eq_top, dense_addSubmonoidClosure_iff_addSubgroupClosure, IsSemilinearSet.closure_of_finite, Subsemigroup.nonUnitalSubsemiringClosure_coe, AddSubgroup.closure_toAddSubmonoid, fg_iff, Rat.addSubmonoid_closure_range_pow, closure_nsmul_le, isProperLinearSet_iff, closure_addSubmonoidClosure_eq_closure_addSubgroupClosure, closure_insert_zero, IsLinearSet.closure, mem_closure_of_mem, unop_closure, smul_closure, pow_eq_closure_pow_set, Submodule.span_eq_closure, Submodule.closure_subset_span, closure_eq, Rat.addSubmonoid_closure_range_mul_self, topologicalClosure_addSubgroupClosure_toAddSubmonoid, DFinsupp.add_closure_iUnion_range_single, closure_closure_coe_preimage, NNRat.addSubmonoid_closure_range_pow, mem_closure_image_pos_iff, AddSubgroup.closure_toAddSubmonoid_of_finite, FreeAddMonoid.closure_range_of, FreeAddMonoid.mrange_lift, AddMonoidHom.mclosure_range, one_eq_closure, closure_add_le, AddSubgroup.closure_toAddSubmonoid_of_isOfFinAddOrder, one_eq_closure_one_set, Submodule.span_nat_eq_addSubmonoidClosure, Int.addSubmonoid_closure_range_pow, IsAddIndecomposable.apply_ne_zero_iff_mem_closure, mem_closure, closure_neg, closure_prod_zero, closure_pow, StarOrderedRing.le_iff, Finsupp.add_closure_setOf_eq_single, mem_closure_iff_of_fintype, sup_eq_closure_add, RootPairing.Base.root_mem_or_neg_mem, closure_eq_image_sum, AddMonoid.Coprod.mclosure_range_inl_union_inr, RootPairing.eq_baseOf_iff, Subsemiring.coe_closure_eq, closure_singleton_zero, StarOrderedRing.nonneg_iff, closure_le, addIrreducible_mem_addSubmonoidClosure_subset, mem_closure_range_iff_of_fintype, FG.exists_minimal_closure_eq, PresentedAddMonoid.closure_range_of, RootPairing.Base.coroot_mem_or_neg_mem, op_closure, AddMonoidHom.eqOn_closureM, Polynomial.addSubmonoid_closure_setOf_eq_monomial, mem_closure_pair, AddSubgroup.le_closure_toAddSubmonoid, Submodule.span_closure, closure_iUnion, Submonoid.toAddSubmonoid'_closure, mem_closure_neg, HomogeneousIdeal.irrelevant_eq_closure, NNRat.addSubmonoid_closure_range_mul_self, IsSemilinearSet.closure, Submonoid.subsemiringClosure_mem, Int.addSubmonoid_closure_range_mul_self, mem_closure_singleton, mem_closure_finset', NonUnitalSubsemiring.mem_closure_iff, Nat.one_mem_closure_iff, closure_eq_mrange, Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid, NonUnitalSubsemiring.coe_closure_eq, closure_empty, AddMonoidAlgebra.mem_closure_of_mem_span_closure, IsAddIndecomposable.mem_or_neg_mem_closure_baseOf, Subsemiring.mem_closure_iff, toSubmonoid'_closure, closure_singleton_le_iff_mem, closure_mul_closure, closure_mono, iSup_eq_closure, mul_eq_closure_mul_set
gi 📖	CompOp	—
instCompleteLattice 📖	CompOp	80 math math: smul_iSup, sup_eq_closure, op_sup, AddCommMonoid.primaryComponent.disjoint, iSup_map_single, fixedPoints_addSubmonoid_iSup, sup_mul, smul_sup, AddMonoid.Coprod.mrange_lift, closure_union, neg_sup, FG.iSup, mul_iSup, disjoint_def', iSup_map_single_le, sup_eq_range, mem_bsupr_iff_exists_dfinsupp, unop_iSup, Submodule.toAddSubmonoid_sSup, mem_iSup, AddSubgroup.ofAddUnits_sSup, mul_sup, AddMonoid.Coprod.codisjoint_mrange_inl_mrange_inr, exists_mem_sup, fixedPoints_addSubmonoid_sup, iSup_eq_mrange_dfinsuppSumAddHom, AddSubgroup.ofAddUnits_inf, coe_iSup_of_directed, coe_sSup_of_directedOn, add_mem_sup, unop_sSup, AddMonoidHom.noncommPiCoprod_mrange, mrange_inl_sup_mrange_inr, bsupr_eq_mrange_dfinsuppSumAddHom, FG.biSup, coe_sup, AddSubgroup.ofAddUnits_iSup₂, op_sSup, op_iSup, mem_iSup_of_directed, closure_add_le, DirectSum.IsInternal.addSubmonoid_iSup_eq_top, sup_eq_closure_add, AddMonoid.Coprod.mrange_inl_sup_mrange_inr, FG.biSup_finset, map_iSup, mem_sup, map_sup_comap_of_surjective, mem_iSup_iff_exists_dfinsupp', AddSubgroup.ofAddUnits_sup_addUnits, AddSubgroup.toAddSubmonoid_zmultiples, mem_iSup_iff_exists_dfinsupp, HomogeneousIdeal.irrelevant_eq_iSup, AddMonoid.Coprod.mrange_eq, disjoint_def, closure_iUnion, mem_sSup_of_mem, Submodule.sup_toAddSubmonoid, map_sup, addSubmonoid_smul_sup, mem_iSup_of_mem, map_iSup_comap_of_surjective, FG.finset_sup, neg_iSup, comap_iSup_map_of_injective, mem_biSup_of_directedOn, prod_bot_sup_bot_prod, iSup_mul, AddSubgroup.ofAddUnits_iSup, FG.sup, unop_sup, Submodule.iSup_toAddSubmonoid, mem_sup_left, DirectSum.IsInternal.addSubmonoid_iSupIndep, mem_sSup_of_directedOn, comap_sup_map_of_injective, iSupIndep_of_dfinsuppSumAddHom_injective, mem_sup_right, iSup_eq_closure, mem_iSup_prop
instInfSet 📖	CompOp	19 math math: neg_iInf, addUnits_iInf₂, addUnits_sInf, comap_iInf, unop_iInf, addUnits_iInf, mem_sInf, coe_iInf, Subsemiring.sInf_toAddSubmonoid, coe_sInf, unop_sInf, mem_iInf, NonUnitalSubsemiring.sInf_toAddSubmonoid, op_sInf, map_iInf_comap_of_surjective, comap_iInf_map_of_injective, map_iInf, op_iInf, fixingAddSubmonoid_iUnion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_empty 📖	mathematical	—	closure Set Set.instEmptyCollection Bot.bot AddSubmonoid instBot	—	GaloisConnection.l_bot GaloisInsertion.gc
closure_eq 📖	mathematical	—	closure SetLike.coe AddSubmonoid instSetLike	—	GaloisInsertion.l_u_eq
closure_eq_of_le 📖	—	Set Set.instHasSubset SetLike.coe AddSubmonoid instSetLike Preorder.toLE PartialOrder.toPreorder instPartialOrder closure	—	—	le_antisymm closure_le
closure_iUnion 📖	mathematical	—	closure Set.iUnion iSup AddSubmonoid CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
closure_induction 📖	—	subset_closure AddZero.toZero AddZeroClass.toAddZero ZeroMemClass.zero_mem AddSubmonoid instSetLike AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass closure AddZero.toAdd AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SetLike.instMembership	—	—	subset_closure ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass closure_le
closure_induction₂ 📖	—	subset_closure AddZero.toZero AddZeroClass.toAddZero ZeroMemClass.zero_mem AddSubmonoid instSetLike AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass closure AddZero.toAdd AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SetLike.instMembership	—	—	subset_closure ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass closure_induction
closure_insert_zero 📖	mathematical	—	closure Set Set.instInsert AddZero.toZero AddZeroClass.toAddZero	—	Set.insert_eq closure_union sup_eq_right closure_singleton_le_iff_mem ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass
closure_le 📖	mathematical	—	AddSubmonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder closure Set Set.instHasSubset SetLike.coe instSetLike	—	Set.Subset.trans subset_closure sInf_le
closure_mono 📖	mathematical	Set Set.instHasSubset	AddSubmonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder closure	—	closure_le Set.Subset.trans subset_closure
closure_sdiff_eq_closure 📖	—	Set Set.instHasSubset SetLike.coe AddSubmonoid instSetLike closure Set.instSDiff	—	—	LE.le.antisymm closure_mono Set.diff_subset closure_le SetLike.mem_coe mem_closure Set.mem_diff_of_mem
closure_sdiff_singleton_zero 📖	mathematical	—	closure Set Set.instSDiff Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero	—	closure_sdiff_eq_closure Set.singleton_subset_iff SetLike.mem_coe ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass
closure_singleton_le_iff_mem 📖	mathematical	—	AddSubmonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder closure Set Set.instSingletonSet SetLike.instMembership instSetLike	—	closure_le Set.singleton_subset_iff SetLike.mem_coe
closure_union 📖	mathematical	—	closure Set Set.instUnion AddSubmonoid SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice	—	GaloisConnection.l_sup GaloisInsertion.gc
closure_univ 📖	mathematical	—	closure Set.univ Top.top AddSubmonoid instTop	—	closure_eq coe_top
coe_iInf 📖	mathematical	—	SetLike.coe AddSubmonoid instSetLike iInf instInfSet Set.iInter	—	Set.biInter_range
coe_sInf 📖	mathematical	—	SetLike.coe AddSubmonoid instSetLike InfSet.sInf instInfSet Set.iInter Set Set.instMembership	—	—
dense_induction 📖	—	closure Top.top AddSubmonoid instTop AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	—	—	closure_induction mem_top
disjoint_def 📖	mathematical	—	Disjoint AddSubmonoid instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice AddZero.toZero AddZeroClass.toAddZero	—	disjoint_iff_inf_le SetLike.le_def instIsConcreteLE mem_inf mem_bot
disjoint_def' 📖	mathematical	—	Disjoint AddSubmonoid instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice AddZero.toZero AddZeroClass.toAddZero	—	disjoint_def
iSup_eq_closure 📖	mathematical	—	iSup AddSubmonoid CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice closure Set.iUnion SetLike.coe instSetLike	—	closure_iUnion closure_eq
mem_closure 📖	mathematical	—	AddSubmonoid SetLike.instMembership instSetLike closure	—	mem_sInf
mem_closure_of_mem 📖	mathematical	Set Set.instMembership	AddSubmonoid SetLike.instMembership instSetLike closure	—	subset_closure
mem_iInf 📖	mathematical	—	AddSubmonoid SetLike.instMembership instSetLike iInf instInfSet	—	mem_sInf Set.forall_mem_range
mem_iSup 📖	mathematical	—	AddSubmonoid SetLike.instMembership instSetLike iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice	—	closure_singleton_le_iff_mem le_iSup_iff
mem_sInf 📖	mathematical	—	AddSubmonoid SetLike.instMembership instSetLike InfSet.sInf instInfSet	—	Set.mem_iInter₂
notMem_of_notMem_closure 📖	mathematical	AddSubmonoid SetLike.instMembership instSetLike closure	Set Set.instMembership	—	subset_closure
subset_closure 📖	mathematical	—	Set Set.instHasSubset SetLike.coe AddSubmonoid instSetLike closure	—	mem_closure
sup_eq_closure 📖	mathematical	—	AddSubmonoid SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice closure Set Set.instUnion SetLike.coe instSetLike	—	closure_union closure_eq

IsAddUnit

Definitions

Name	Category	Theorems
addSubmonoid 📖	CompOp	6 math math: AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddSubmonoid.leftNeg_le_isAddUnit, AddSubmonoid.IsUnit.Submonoid.coe_neg, mem_addSubmonoid_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_addSubmonoid_iff 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike addSubmonoid IsAddUnit	—	Set.mem_setOf_eq

IsUnit

Definitions

Name	Category	Theorems
submonoid 📖	CompOp	21 math math: IsFractionRing.nonZeroDivisors_eq_isUnit, isUnit_le_nonZeroDivisors, Algebra.essFiniteType_cond_iff, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, IsArtinianRing.isUnitSubmonoid_eq_of_mulOpposite, Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe, mem_submonoid_iff, IsArtinianRing.nonZeroDivisorsLeft_eq_isUnitSubmonoid, Submodule.mker_spanSingleton, IsArtinianRing.isUnit_submonoid_eq, le_isUnit_iff_zero_notMem, IsLocalization.submonoid_map_le_is_unit, Submonoid.leftInv_le_isUnit, IsArtinianRing.isUnit_submonoid_eq_of_isIntegral, IsArtinianRing.isUnitSubmonoid_eq, IsFractionRing.self_iff_nonZeroDivisors_le_isUnit, Algebra.EssFiniteType.cond, Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply, Submonoid.IsUnit.Submonoid.coe_inv, IsFractionRing.self_iff_nonZeroDivisors_eq_isUnit, IsArtinianRing.isUnitSubmonoid_eq_nonZeroDivisorsRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_submonoid_iff 📖	mathematical	—	Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike submonoid IsUnit	—	Set.mem_setOf_eq

MonoidHom

Definitions

Name	Category	Theorems
ofClosureMEqTopLeft 📖	CompOp	1 math math: coe_ofClosureMEqTopLeft
ofClosureMEqTopRight 📖	CompOp	1 math math: coe_ofClosureMEqTopRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofClosureMEqTopLeft 📖	mathematical	Submonoid.closure Monoid.toMulOneClass Top.top Submonoid Submonoid.instTop MulOne.toOne MulOneClass.toMulOne MulOne.toMul	DFunLike.coe MonoidHom instFunLike ofClosureMEqTopLeft	—	—
coe_ofClosureMEqTopRight 📖	mathematical	Submonoid.closure Monoid.toMulOneClass Top.top Submonoid Submonoid.instTop MulOne.toOne MulOneClass.toMulOne MulOne.toMul	DFunLike.coe MonoidHom instFunLike ofClosureMEqTopRight	—	—
eqOn_closureM 📖	mathematical	Set.EqOn DFunLike.coe MonoidHom MulOneClass.toMulOne instFunLike	SetLike.coe Submonoid Submonoid.instSetLike Submonoid.closure	—	Submonoid.closure_le
eq_of_eqOn_denseM 📖	—	Submonoid.closure Top.top Submonoid Submonoid.instTop Set.EqOn DFunLike.coe MonoidHom MulOneClass.toMulOne instFunLike	—	—	eq_of_eqOn_topM eqOn_closureM

Submonoid

Definitions

Name	Category	Theorems
closure 📖	CompOp	93 math math: mem_closure_iff_of_fintype, MonoidHom.eqOn_closureM, closure_pow, IsMulIndecomposable.mem_or_inv_mem_closure_baseOf, closure_singleton_le_iff_mem, mem_closure, RootPairing.weylGroup_toSubmonoid, closure_pow_le, mem_closure_singleton_self, closure_pi, Subgroup.closure_toSubmonoid, Equiv.Perm.mclosure_swap_castSucc_succ, Set.IsPWO.submonoid_closure, iSup_eq_closure, Commute.exists_orderOf_eq_lcm, toAddSubmonoid_closure, sup_eq_closure_mul, Monoid.CoprodI.mclosure_iUnion_range_of, PresentedMonoid.closure_range_of, closure_eq_one_union, closure_singleton_eq, closure_univ, exists_minimal_closure_eq_top, FreeMonoid.closure_range_of, AddSubmonoid.toSubmonoid_closure, Subring.mem_closure_iff, powers_eq_closure, mem_closure_singleton, closure_mono, mul_subset_closure, Algebra.adjoin_toSubmodule_le, closure_prod_one, closure_eq, topologicalClosure_subgroupClosure_toSubmonoid, Subgroup.le_closure_toSubmonoid, Monoid.closure_finset_fg, closure_le_centralizer_centralizer, Monoid.fg_iff, MonoidHom.mclosure_preimage_le, FreeMonoid.mrange_lift, closure_mul_le, dense_submonoidClosure_iff_subgroupClosure, closure_submonoidClosure_eq_closure_subgroupClosure, Algebra.adjoin_eq_span, fg_iff, Subsemiring.coe_closure_eq, MonoidWithZeroHom.valueMonoid_eq_closure, closure_empty, closure_prod, closure_sdiff_singleton_one, mem_closure_finset, closure_image_isMulIndecomposable_baseOf, op_closure, mem_closure_range_iff, smul_closure, closure_insert_one, mem_closure_range_iff_of_fintype, closure_union, mem_closure_inv, Monoid.Coprod.mclosure_range_inl_union_inr, StarAlgebra.adjoin_eq_span, toAddSubmonoid'_closure, Subsemiring.closure_submonoid_closure, mem_closure_finset', Monoid.closure_finite_fg, irreducible_mem_submonoidClosure_subset, closure_singleton_one, MonoidHom.map_mclosure, closure_iUnion, mem_closure_of_mem, closure_image_one_lt_and_isMulIndecomposable, CoxeterSystem.submonoid_closure_range_simple, closure_closure_coe_preimage, Equiv.Perm.mclosure_isSwap, closure_inv, MonoidHom.mclosure_range, unop_closure, closure_irreducible, subset_closure, FG.exists_minimal_closure_eq, IsMulIndecomposable.apply_ne_one_iff_mem_closure, Subgroup.closure_toSubmonoid_of_isOfFinOrder, Subsemiring.mem_closure_iff, sup_eq_closure, closure_le, mem_closure_pair, mem_closure_iff_exists_finset_subset, mem_closure_image_one_lt_iff, Subgroup.closure_toSubmonoid_of_finite, AddSubmonoid.toSubmonoid'_closure, closure_eq_mrange, closure_eq_image_prod, closure_one_prod
gi 📖	CompOp	—
instCompleteLattice 📖	CompOp	64 math math: comap_sup_map_of_injective, unop_iSup, coe_iSup_of_directed, map_sup_comap_of_surjective, mem_sup, iSup_eq_closure, coe_sSup_of_directedOn, mrange_inl_sup_mrange_inr, prod_bot_sup_bot_prod, mem_iSup, Monoid.CoprodI.mrange_eq_iSup, iSup_map_mulSingle_le, Monoid.Coprod.mrange_eq, sup_eq_closure_mul, mem_sup_left, mem_sSup_of_directedOn, op_sSup, fixedPoints_submonoid_sup, smul_sup, FG.finset_sup, map_iSup, iSup_map_mulSingle, map_sup, op_iSup, inv_sup, Subgroup.toSubmonoid_zpowers, mem_iSup_prop, Subgroup.ofUnits_inf, Monoid.Coprod.mrange_lift, map_iSup_comap_of_surjective, comap_iSup_map_of_injective, op_sup, CommMonoid.primaryComponent.disjoint, inv_iSup, fixedPoints_submonoid_iSup, mem_iSup_of_directed, unop_sup, MonoidHom.noncommPiCoprod_mrange, FG.iSup, closure_mul_le, mul_mem_sup, coe_sup, Monoid.CoprodI.iSup_mrange_of, unop_sSup, mem_sup_right, FG.sup, mem_biSup_of_directedOn, Subgroup.ofUnits_iSup₂, closure_union, mem_sSup_of_mem, Subgroup.ofUnits_sSup, mem_iSup_of_mem, closure_iUnion, disjoint_def', FG.biSup_finset, sup_eq_range, disjoint_def, Subgroup.ofUnits_iSup, Monoid.Coprod.mrange_inl_sup_mrange_inr, Monoid.Coprod.codisjoint_mrange_inl_mrange_inr, sup_eq_closure, exists_mem_sup, Subgroup.ofUnits_sup_units, FG.biSup
instInfSet 📖	CompOp	20 math math: units_iInf, comap_iInf, op_iInf, unop_iInf, comap_iInf_map_of_injective, op_sInf, mem_sInf, units_sInf, unop_sInf, fixingSubmonoid_iUnion, mem_iInf, units_iInf₂, map_iInf, Subring.sInf_toSubmonoid, inv_iInf, coe_iInf, Subsemiring.sInf_toSubmonoid, coe_sInf, map_iInf_comap_of_surjective, TopCat.Presheaf.submonoidPresheafOfStalk_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_empty 📖	mathematical	—	closure Set Set.instEmptyCollection Bot.bot Submonoid instBot	—	GaloisConnection.l_bot GaloisInsertion.gc
closure_eq 📖	mathematical	—	closure SetLike.coe Submonoid instSetLike	—	GaloisInsertion.l_u_eq
closure_eq_of_le 📖	—	Set Set.instHasSubset SetLike.coe Submonoid instSetLike Preorder.toLE PartialOrder.toPreorder instPartialOrder closure	—	—	le_antisymm closure_le
closure_eq_one_union 📖	mathematical	—	SetLike.coe Submonoid instSetLike closure Set Set.instUnion Set.instSingletonSet MulOne.toOne MulOneClass.toMulOne Subsemigroup MulOne.toMul Subsemigroup.instSetLike Subsemigroup.closure	—	le_antisymm closure_induction Subsemigroup.subset_closure mul_one one_mul MulMemClass.mul_mem Subsemigroup.instMulMemClass OneMemClass.one_mem SubmonoidClass.toOneMemClass instSubmonoidClass Subsemigroup.closure_le subset_closure
closure_iUnion 📖	mathematical	—	closure Set.iUnion iSup Submonoid CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
closure_induction 📖	—	subset_closure MulOne.toOne MulOneClass.toMulOne OneMemClass.one_mem Submonoid instSetLike SubmonoidClass.toOneMemClass instSubmonoidClass closure MulOne.toMul MulMemClass.mul_mem SubmonoidClass.toMulMemClass SetLike.instMembership	—	—	subset_closure OneMemClass.one_mem SubmonoidClass.toOneMemClass instSubmonoidClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass closure_le
closure_induction₂ 📖	—	subset_closure MulOne.toOne MulOneClass.toMulOne OneMemClass.one_mem Submonoid instSetLike SubmonoidClass.toOneMemClass instSubmonoidClass closure MulOne.toMul MulMemClass.mul_mem SubmonoidClass.toMulMemClass SetLike.instMembership	—	—	subset_closure OneMemClass.one_mem SubmonoidClass.toOneMemClass instSubmonoidClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass closure_induction
closure_insert_one 📖	mathematical	—	closure Set Set.instInsert MulOne.toOne MulOneClass.toMulOne	—	Set.insert_eq closure_union sup_eq_right closure_singleton_le_iff_mem OneMemClass.one_mem SubmonoidClass.toOneMemClass instSubmonoidClass
closure_le 📖	mathematical	—	Submonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder closure Set Set.instHasSubset SetLike.coe instSetLike	—	Set.Subset.trans subset_closure sInf_le
closure_mono 📖	mathematical	Set Set.instHasSubset	Submonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder closure	—	closure_le Set.Subset.trans subset_closure
closure_sdiff_eq_closure 📖	—	Set Set.instHasSubset SetLike.coe Submonoid instSetLike closure Set.instSDiff	—	—	LE.le.antisymm closure_mono Set.diff_subset closure_le SetLike.mem_coe mem_closure Set.mem_diff_of_mem
closure_sdiff_singleton_one 📖	mathematical	—	closure Set Set.instSDiff Set.instSingletonSet MulOne.toOne MulOneClass.toMulOne	—	closure_sdiff_eq_closure SubmonoidClass.toOneMemClass instSubmonoidClass
closure_singleton_le_iff_mem 📖	mathematical	—	Submonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder closure Set Set.instSingletonSet SetLike.instMembership instSetLike	—	closure_le Set.singleton_subset_iff SetLike.mem_coe
closure_union 📖	mathematical	—	closure Set Set.instUnion Submonoid SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice	—	GaloisConnection.l_sup GaloisInsertion.gc
closure_univ 📖	mathematical	—	closure Set.univ Top.top Submonoid instTop	—	closure_eq coe_top
coe_iInf 📖	mathematical	—	SetLike.coe Submonoid instSetLike iInf instInfSet Set.iInter	—	Set.biInter_range
coe_sInf 📖	mathematical	—	SetLike.coe Submonoid instSetLike InfSet.sInf instInfSet Set.iInter Set Set.instMembership	—	—
dense_induction 📖	—	closure Top.top Submonoid instTop MulOne.toOne MulOneClass.toMulOne MulOne.toMul	—	—	closure_induction mem_top
disjoint_def 📖	mathematical	—	Disjoint Submonoid instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice MulOne.toOne MulOneClass.toMulOne	—	instIsConcreteLE
disjoint_def' 📖	mathematical	—	Disjoint Submonoid instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice MulOne.toOne MulOneClass.toMulOne	—	disjoint_def
iSup_eq_closure 📖	mathematical	—	iSup Submonoid CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice closure Set.iUnion SetLike.coe instSetLike	—	closure_iUnion closure_eq
mem_closure 📖	mathematical	—	Submonoid SetLike.instMembership instSetLike closure	—	mem_sInf
mem_closure_of_mem 📖	mathematical	Set Set.instMembership	Submonoid SetLike.instMembership instSetLike closure	—	subset_closure
mem_iInf 📖	mathematical	—	Submonoid SetLike.instMembership instSetLike iInf instInfSet	—	—
mem_iSup 📖	mathematical	—	Submonoid SetLike.instMembership instSetLike iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice	—	closure_singleton_le_iff_mem le_iSup_iff
mem_sInf 📖	mathematical	—	Submonoid SetLike.instMembership instSetLike InfSet.sInf instInfSet	—	Set.mem_iInter₂
notMem_of_notMem_closure 📖	mathematical	Submonoid SetLike.instMembership instSetLike closure	Set Set.instMembership	—	subset_closure
subset_closure 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Submonoid instSetLike closure	—	mem_closure
sup_eq_closure 📖	mathematical	—	Submonoid SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice closure Set Set.instUnion SetLike.coe instSetLike	—	closure_union closure_eq

---

← Back to Index