Defs

📁 Source: Mathlib/Algebra/Group/Subsemigroup/Defs.lean

Statistics

Metric	Count
Definitions `eqLocus`, `AddMemClass`, `add`, `subtype`, `toAddCommSemigroup`, `toAddSemigroup`, `AddSubsemigroup`, `carrier`, `copy`, `instBot`, `instInhabited`, `instMin`, `instPartialOrder`, `instSetLike`, `instTop`, `ofClass`, `eqLocus`, `MulMemClass`, `mul`, `subtype`, `toCommSemigroup`, `toSemigroup`, `Subsemigroup`, `carrier`, `copy`, `instBot`, `instInhabited`, `instMin`, `instPartialOrder`, `instSetLike`, `instTop`, `ofClass`	32
Theorems `eq_of_eqOn_top`, `mem_eqLocus`, `add_def`, `add_mem`, `coe_add`, `coe_subtype`, `isCancelAdd`, `isLeftCancelAdd`, `isRightCancelAdd`, `mk_add_mk`, `subtype_apply`, `subtype_injective`, `add_mem`, `add_mem'`, `coe_bot`, `coe_copy`, `coe_inf`, `coe_ofClass`, `coe_set_mk`, `coe_top`, `copy_eq`, `ext`, `ext_iff`, `instAddMemClass`, `instCanLiftSetCoeForallForallForallMemForallHAdd`, `instNontrivialOfNonempty`, `mem_carrier`, `mem_inf`, `mem_mk`, `mem_top`, `mk_eq_bot`, `mk_eq_top`, `mk_le_mk`, `notMem_bot`, `subsingleton_of_subsingleton`, `of_setLike_add_comm`, `of_setLike_mul_comm`, `eq_of_eqOn_top`, `mem_eqLocus`, `coe_mul`, `coe_subtype`, `isCancelMul`, `isLeftCancelMul`, `isRightCancelMul`, `mk_mul_mk`, `mul_def`, `mul_mem`, `subtype_apply`, `subtype_injective`, `coe_bot`, `coe_copy`, `coe_inf`, `coe_ofClass`, `coe_set_mk`, `coe_top`, `copy_eq`, `ext`, `ext_iff`, `instCanLiftSetCoeForallForallForallMemForallHMul`, `instMulMemClass`, `instNontrivialOfNonempty`, `mem_carrier`, `mem_inf`, `mem_mk`, `mem_top`, `mk_eq_bot`, `mk_eq_top`, `mk_le_mk`, `mul_mem`, `mul_mem'`, `notMem_bot`, `subsingleton_of_subsingleton`, `isAddCommutative_iff_of_setLike`, `isMulCommutative_iff_of_setLike`, `setLike_add_comm`, `setLike_mul_comm`	76
Total	108

AddHom

Definitions

Name	Category	Theorems
`eqLocus` 📖	CompOp	1 math math: `mem_eqLocus`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_eqOn_top` 📖	—	`Set.EqOn` `DFunLike.coe` `AddHom` `funLike` `SetLike.coe` `AddSubsemigroup` `AddSubsemigroup.instSetLike` `Top.top` `AddSubsemigroup.instTop`	—	—	`ext`
`mem_eqLocus` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `eqLocus` `DFunLike.coe` `AddHom` `funLike`	—	—

AddMemClass

Definitions

Name	Category	Theorems
`add` 📖	CompOp	30 math math: `AddHom.coe_srangeRestrict`, `AddHom.subsemigroupMap_apply_coe`, `isRightCancelAdd`, `AddHom.srangeRestrict_surjective`, `AddHom.subsemigroupMap_surjective`, `AddSubsemigroup.topEquiv_apply`, `add_def`, `AddHom.codRestrict_apply_coe`, `AddEquiv.ofLeftInverse_apply`, `AddSubsemigroup.topEquiv_symm_apply_coe`, `AddEquiv.subsemigroupMap_apply_coe`, `coe_add`, `AddSubsemigroup.closure_closure_coe_preimage`, `subtype_apply`, `isAddCommutative_iff_of_setLike`, `AddSubsemigroup.strictMono_topEquiv`, `AddEquiv.strictMono_subsemigroupCongr`, `AddSubsemigroup.coe_equivMapOfInjective_apply`, `AddSubsemigroup.range_subtype`, `coe_subtype`, `isCancelAdd`, `IsAddCommutative.of_setLike_add_comm`, `AddHom.subsemigroupComap_apply_coe`, `mk_add_mk`, `AddEquiv.subsemigroupMap_symm_apply_coe`, `AddSubsemigroup.topEquiv_toAddHom`, `subtype_injective`, `AddHom.restrict_apply`, `AddEquiv.ofLeftInverse_symm_apply`, `isLeftCancelAdd`
`subtype` 📖	CompOp	5 math math: `subtype_apply`, `AddSubsemigroup.range_subtype`, `coe_subtype`, `AddSubsemigroup.topEquiv_toAddHom`, `subtype_injective`
`toAddCommSemigroup` 📖	CompOp	2 math math: `LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle`, `LieSubmodule.coe_add`
`toAddSemigroup` 📖	CompOp	4 math math: `AddSubsemigroup.continuousAdd`, `AddSubsemigroup.isAddCommutative_closure`, `AddSubsemigroup.separatelyContinuousAdd`, `AddSubsemigroup.instIsAddCommutative_closure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_def` 📖	mathematical	—	`SetLike.instMembership` `add` `add_mem`	—	—
`add_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership`	—	—
`coe_add` 📖	mathematical	—	`SetLike.instMembership` `add`	—	—
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `AddHom` `SetLike.instMembership` `add` `AddHom.funLike` `subtype`	—	—
`isCancelAdd` 📖	mathematical	—	`IsCancelAdd` `SetLike.instMembership` `add`	—	`isLeftCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `isRightCancelAdd` `IsCancelAdd.toIsRightCancelAdd`
`isLeftCancelAdd` 📖	mathematical	—	`IsLeftCancelAdd` `SetLike.instMembership` `add`	—	`Function.Injective.isLeftCancelAdd` `Subtype.coe_injective`
`isRightCancelAdd` 📖	mathematical	—	`IsRightCancelAdd` `SetLike.instMembership` `add`	—	`Function.Injective.isRightCancelAdd` `Subtype.coe_injective`
`mk_add_mk` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `add` `add_mem`	—	—
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `SetLike.instMembership` `add` `AddHom.funLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `AddHom` `add` `AddHom.funLike` `subtype`	—	`Subtype.coe_injective`

AddSubsemigroup

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	50 math math: `NonUnitalStarSubalgebra.mem_carrier`, `ClosedSubmodule.mem_iff`, `ClosedAddSubgroup.ext_iff`, `Submodule.toSubalgebra_toSubsemiring`, `Subalgebra.coe_center`, `ClosedSubmodule.coe_sSup`, `Submodule.coe_toSubalgebra`, `Submodule.smul_mem'`, `Subring.coe_matrix`, `LieSubalgebra.mem_carrier`, `HahnSeries.cardSuppLTSubfield_carrier`, `ClosedSubmodule.ext_iff`, `NonUnitalStarSubsemiring.star_mem'`, `ClosedAddSubgroup.isClosed'`, `mem_carrier`, `FiniteIndexNormalAddSubgroup.ext_iff`, `Subsemiring.center_toSubmonoid`, `NonUnitalSubalgebra.smul_mem'`, `NonUnitalStarSubsemiring.mem_carrier`, `LieSubmodule.lie_mem`, `Subalgebra.coe_matrix`, `AddSubmonoid.mem_carrier`, `add_mem'`, `ClosedSubmodule.mem_sup`, `ClosedSubmodule.mem_iSup`, `NonUnitalSubsemiring.mem_carrier`, `NonUnitalSubsemiring.mul_mem'`, `AddSubgroup.mem_carrier`, `Representation.invariants_eq_inter`, `NonUnitalSubalgebra.mem_carrier`, `Subalgebra.pi_toSubsemiring`, `ClosedSubmodule.mem_sSup`, `OpenAddSubgroup.isOpen'`, `Submodule.mem_carrier`, `Subalgebra.coe_pi`, `AddSubmonoid.zero_mem'`, `Subsemiring.coe_matrix`, `NonUnitalStarSubalgebra.star_mem'`, `NonUnitalSubring.neg_mem'`, `LieSubmodule.mem_carrier`, `ClosedSubmodule.coe_iSup`, `AddSubgroup.neg_mem'`, `Subsemiring.coe_center`, `ClosedSubmodule.coe_sup`, `Submodule.carrier_eq_coe`, `LieSubalgebra.lie_mem'`, `ClosedSubmodule.carrier_eq_coe`, `OpenNormalAddSubgroup.ext_iff`, `Subsemiring.coe_nonneg`, `ClosedSubmodule.isClosed'`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`instBot` 📖	CompOp	10 math math: `notMem_bot`, `coe_bot`, `op_eq_bot`, `unop_eq_bot`, `map_bot`, `bot_prod_bot`, `unop_bot`, `op_bot`, `mk_eq_bot`, `closure_empty`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	9 math math: `map_inf_comap_of_surjective`, `coe_inf`, `comap_inf`, `map_comap_eq`, `comap_inf_map_of_injective`, `unop_inf`, `mem_inf`, `map_inf`, `op_inf`
`instPartialOrder` 📖	CompOp	41 math math: `closure_le_centralizer_centralizer`, `coe_toSubsemigroup_symm_apply`, `le_op_iff`, `coe_toSubsemigroup_apply`, `center_le_centralizer`, `op_le_iff`, `toSubsemigroup'_closure`, `map_le_map_iff_of_injective`, `centralizer_le`, `le_comap_map`, `le_prod_iff`, `opEquiv_symm_apply`, `topologicalClosure_minimal`, `op_le_op_iff`, `Subsemigroup.toAddSubsemigroup_closure`, `closure_singleton_le_iff_mem`, `comap_strictMono_of_surjective`, `ArchimedeanClass.subsemigroup_strictAnti`, `closure_le`, `topologicalClosure_mono`, `map_comap_le`, `le_comap_of_map_le`, `mk_le_mk`, `unop_le_unop_iff`, `monotone_comap`, `Subsemigroup.coe_toAddSubsemigroup_symm_apply`, `prod_mono`, `AddSubmonoid.mk_le_mk`, `map_le_iff_le_comap`, `map_strictMono_of_injective`, `toSubsemigroup_closure`, `comap_le_comap_iff_of_surjective`, `opEquiv_apply`, `AddHom.mclosure_preimage_le`, `closure_mono`, `monotone_map`, `Subsemigroup.toAddSubsemigroup'_closure`, `le_topologicalClosure`, `map_le_of_le_comap`, `gc_map_comap`, `Subsemigroup.coe_toAddSubsemigroup_apply`
`instSetLike` 📖	CompOp	114 math math: `AddSubgroup.centerToAddOpposite_apply_coe`, `ArchimedeanClass.subsemigroup_eq_addSubgroup_of_ne_top`, `add_mem`, `closure_le_centralizer_centralizer`, `AddHom.coe_srangeRestrict`, `AddHom.subsemigroupMap_apply_coe`, `mem_closure`, `coe_toSubsemigroup_symm_apply`, `coe_inf`, `AddHom.srangeRestrict_surjective`, `mem_map_equiv`, `coe_toSubsemigroup_apply`, `coe_iSup_of_directed`, `AddHom.subsemigroupMap_surjective`, `mem_centralizer_iff`, `notMem_bot`, `AddSubmonoid.centerCongr_symm_apply_coe`, `coe_top`, `coe_prod`, `coe_bot`, `topEquiv_apply`, `mem_closure_of_mem`, `AddSubmonoid.centerToAddOpposite_symm_apply_coe`, `mem_unop`, `centerToAddOpposite_symm_apply_coe`, `AddHom.eqOn_closure`, `mem_center_iff`, `mem_iSup`, `mem_map_of_mem`, `mem_biSup_of_directedOn`, `continuousAdd`, `mem_mk`, `coe_sumNonzeroSq`, `mem_sup_left`, `mem_prod`, `AddEquiv.ofLeftInverse_apply`, `topEquiv_symm_apply_coe`, `instAddMemClass`, `AddSubgroup.centerCongr_apply_coe`, `AddEquiv.subsemigroupMap_apply_coe`, `mem_iSup_of_mem`, `subset_closure`, `centerCongr_apply_coe`, `instCanLiftSetCoeForallForallForallMemForallHAdd`, `mem_carrier`, `closure_closure_coe_preimage`, `coe_map`, `mem_iInf`, `isAddCommutative_closure`, `closure_eq`, `FiniteArchimedeanClass.subsemigroup_eq_addSubgroup`, `coe_sInf`, `strictMono_topEquiv`, `closure_singleton_le_iff_mem`, `mem_sInf`, `AddEquiv.strictMono_subsemigroupCongr`, `coe_equivMapOfInjective_apply`, `iSup_eq_closure`, `AddSubgroup.centerCongr_symm_apply_coe`, `range_subtype`, `coe_unop`, `closure_le`, `mem_top`, `coe_topologicalClosure`, `mem_sup_right`, `centralizer_eq_top_iff_subset`, `mem_comap`, `centerCongr_symm_apply_coe`, `eq_top_iff'`, `mem_map`, `AddSubmonoid.mem_mk`, `equivOp_symm_apply_coe`, `mem_sumNonzeroSq`, `mem_op`, `coe_centralizer`, `mem_sSup_of_mem`, `AddSubgroup.centerToAddOpposite_symm_apply_coe`, `AddSubmonoid.centerCongr_apply_coe`, `Subsemigroup.coe_toAddSubsemigroup_symm_apply`, `mem_inf`, `AddHom.subsemigroupComap_apply_coe`, `coe_comap`, `mem_iSup_prop`, `mem_map_iff_mem`, `mem_sSup_of_directed_on`, `coe_sSup_of_directed_on`, `AddEquiv.subsemigroupMap_symm_apply_coe`, `top_closure_add_self_subset`, `topEquiv_toAddHom`, `coe_set_mk`, `add_mem_sup`, `mem_iSup_of_directed`, `separatelyContinuousAdd`, `AddHom.mem_eqLocus`, `equivOp_apply_coe`, `isClosed_topologicalClosure`, `AddHom.mem_srange`, `coe_iInf`, `centerToAddOpposite_apply_coe`, `mem_even`, `apply_coe_mem_map`, `ext_iff`, `coe_ofClass`, `coe_even`, `AddSubmonoid.coe_set_mk`, `instIsAddCommutative_closure`, `AddEquiv.ofLeftInverse_symm_apply`, `AddSubmonoid.mem_toSubsemigroup`, `coe_op`, `AddHom.coe_srange`, `Subsemigroup.coe_toAddSubsemigroup_apply`, `AddSubmonoid.centerToAddOpposite_apply_coe`, `coe_copy`, `AddSubmonoid.mk_eq_bot`
`instTop` 📖	CompOp	28 math math: `center_eq_top`, `closure_univ`, `prod_eq_top_iff`, `op_eq_top`, `coe_top`, `AddHom.srange_eq_top_of_surjective`, `topEquiv_apply`, `op_top`, `AddHom.srange_eq_top_iff_surjective`, `srange_snd`, `topEquiv_symm_apply_coe`, `top_prod_top`, `closure_closure_coe_preimage`, `strictMono_topEquiv`, `AddHom.srange_eq_map`, `map_equiv_top`, `mem_top`, `unop_top`, `centralizer_eq_top_iff_subset`, `eq_top_iff'`, `comap_top`, `top_prod`, `mk_eq_top`, `AddSubmonoid.mk_eq_top`, `topEquiv_toAddHom`, `srange_fst`, `prod_top`, `unop_eq_top`
`ofClass` 📖	CompOp	1 math math: `coe_ofClass`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem` 📖	mathematical	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	—	`add_mem'`
`add_mem'` 📖	mathematical	`Set` `Set.instMembership` `carrier`	`Set` `Set.instMembership` `carrier`	—	—
`coe_bot` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `AddSubsemigroup` `instSetLike`	`SetLike.coe` `AddSubsemigroup` `instSetLike` `copy`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_ofClass` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `instSetLike` `ofClass`	—	—
`coe_set_mk` 📖	mathematical	`Set` `Set.instMembership`	`SetLike.coe` `AddSubsemigroup` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `AddSubsemigroup` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	—	`ext`
`instAddMemClass` 📖	mathematical	—	`AddMemClass` `AddSubsemigroup` `instSetLike`	—	`add_mem'`
`instCanLiftSetCoeForallForallForallMemForallHAdd` 📖	mathematical	—	`CanLift` `Set` `AddSubsemigroup` `SetLike.coe` `instSetLike`	—	—
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `AddSubsemigroup`	—	`mem_top` `notMem_bot`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `carrier` `AddSubsemigroup` `SetLike.instMembership` `instSetLike`	—	—
`mem_inf` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_mk` 📖	mathematical	`Set` `Set.instMembership`	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership`	—	—
`mem_top` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`mk_eq_bot` 📖	mathematical	`Set` `Set.instMembership`	`Bot.bot` `AddSubsemigroup` `instBot` `Set` `Set.instEmptyCollection`	—	`SetLike.coe_set_eq`
`mk_eq_top` 📖	mathematical	`Set` `Set.instMembership`	`Top.top` `AddSubsemigroup` `instTop` `Set.univ`	—	`SetLike.coe_set_eq`
`mk_le_mk` 📖	mathematical	`Set` `Set.instMembership`	`AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instHasSubset`	—	—
`notMem_bot` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`Set.notMem_empty`
`subsingleton_of_subsingleton` 📖	—	—	—	—	`mem_top` `notMem_bot`

IsAddCommutative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_setLike_add_comm` 📖	mathematical	—	`IsAddCommutative` `SetLike.instMembership` `AddMemClass.add`	—	`isAddCommutative_iff_of_setLike`

IsMulCommutative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_setLike_mul_comm` 📖	mathematical	—	`IsMulCommutative` `SetLike.instMembership` `MulMemClass.mul`	—	`isMulCommutative_iff_of_setLike`

MulHom

Definitions

Name	Category	Theorems
`eqLocus` 📖	CompOp	1 math math: `mem_eqLocus`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_eqOn_top` 📖	—	`Set.EqOn` `DFunLike.coe` `MulHom` `funLike` `SetLike.coe` `Subsemigroup` `Subsemigroup.instSetLike` `Top.top` `Subsemigroup.instTop`	—	—	`ext`
`mem_eqLocus` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `Subsemigroup.instSetLike` `eqLocus` `DFunLike.coe` `MulHom` `funLike`	—	—

MulMemClass

Definitions

Name	Category	Theorems
`mul` 📖	CompOp	35 math math: `SetLike.instSMulCommClass`, `isLeftCancelMul`, `subtype_apply`, `MulHom.subsemigroupComap_apply_coe`, `isCancelMul`, `MulHom.coe_srangeRestrict`, `mul_def`, `Subsemigroup.topEquiv_symm_apply_coe`, `MulEquiv.ofLeftInverse_symm_apply`, `MulEquiv.strictMono_subsemigroupCongr`, `MulHom.restrict_apply`, `coe_subtype`, `Subsemigroup.topEquiv_toMulHom`, `IsMulCommutative.of_setLike_mul_comm`, `MulHom.subsemigroupMap_surjective`, `MulEquiv.ofLeftInverse_apply`, `Subsemigroup.strictMono_topEquiv`, `Subsemigroup.range_subtype`, `SetLike.instIsScalarTower`, `MulZeroMemClass.isLeftCancelMulZero`, `Subsemigroup.closure_closure_coe_preimage`, `Subsemigroup.topEquiv_apply`, `MulZeroMemClass.isRightCancelMulZero`, `mk_mul_mk`, `MulZeroMemClass.isCancelMulZero`, `coe_mul`, `MulHom.srangeRestrict_surjective`, `MulHom.subsemigroupMap_apply_coe`, `isMulCommutative_iff_of_setLike`, `MulEquiv.subsemigroupMap_apply_coe`, `MulEquiv.subsemigroupMap_symm_apply_coe`, `Subsemigroup.coe_equivMapOfInjective_apply`, `MulHom.codRestrict_apply_coe`, `subtype_injective`, `isRightCancelMul`
`subtype` 📖	CompOp	5 math math: `subtype_apply`, `coe_subtype`, `Subsemigroup.topEquiv_toMulHom`, `Subsemigroup.range_subtype`, `subtype_injective`
`toCommSemigroup` 📖	CompOp	—
`toSemigroup` 📖	CompOp	5 math math: `nonZeroDivisors_dvd_iff_dvd_coe`, `Subsemigroup.separatelyContinuousMul`, `Subsemigroup.continuousMul`, `Subsemigroup.isMulCommutative_closure`, `Subsemigroup.instIsMulCommutative_closure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mul` 📖	mathematical	—	`SetLike.instMembership` `mul`	—	—
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `MulHom` `SetLike.instMembership` `mul` `MulHom.funLike` `subtype`	—	—
`isCancelMul` 📖	mathematical	—	`IsCancelMul` `SetLike.instMembership` `mul`	—	`isLeftCancelMul` `IsCancelMul.toIsLeftCancelMul` `isRightCancelMul` `IsCancelMul.toIsRightCancelMul`
`isLeftCancelMul` 📖	mathematical	—	`IsLeftCancelMul` `SetLike.instMembership` `mul`	—	`Function.Injective.isLeftCancelMul` `Subtype.coe_injective`
`isRightCancelMul` 📖	mathematical	—	`IsRightCancelMul` `SetLike.instMembership` `mul`	—	`Function.Injective.isRightCancelMul` `Subtype.coe_injective`
`mk_mul_mk` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `mul` `mul_mem`	—	—
`mul_def` 📖	mathematical	—	`SetLike.instMembership` `mul` `mul_mem`	—	—
`mul_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership`	—	—
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `SetLike.instMembership` `mul` `MulHom.funLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `MulHom` `mul` `MulHom.funLike` `subtype`	—	`Subtype.coe_injective`

Subsemigroup

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	38 math math: `RingPreordering.ext_iff`, `Subsemiring.mem_carrier`, `InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois`, `IntermediateField.mem_carrier`, `ClosedSubgroup.isClosed'`, `FiniteIndexNormalSubgroup.ext_iff`, `Subring.neg_mem'`, `IntermediateField.inv_mem'`, `VonNeumannAlgebra.centralizer_centralizer'`, `StarSubsemiring.mem_carrier`, `Subalgebra.mem_carrier`, `ValuationSubring.mem_carrier`, `Subsemiring.coe_carrier_toSubmonoid`, `Subsemiring.add_mem'`, `StarSubalgebra.star_mem'`, `Subalgebra.algebraMap_mem'`, `RingPreordering.neg_one_notMem'`, `ClosedSubgroup.ext_iff`, `Subfield.coe_inf`, `OpenSubgroup.isOpen'`, `StarSubalgebra.mem_carrier`, `Submonoid.mem_carrier`, `InfiniteGalois.isOpen_iff_finite`, `ValuationSubring.mem_or_inv_mem'`, `StarSubsemiring.star_mem'`, `Subring.mem_carrier`, `Subgroup.inv_mem'`, `RingPreordering.mem_of_isSquare'`, `OpenNormalSubgroup.ext_iff`, `Submonoid.one_mem'`, `SubStarSemigroup.star_mem'`, `Subsemiring.zero_mem'`, `mem_galBasis_iff`, `mul_mem'`, `Subgroup.mem_carrier`, `Subfield.mem_carrier`, `Subfield.inv_mem'`, `mem_carrier`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`instBot` 📖	CompOp	10 math math: `closure_empty`, `notMem_bot`, `unop_eq_bot`, `mk_eq_bot`, `op_bot`, `map_bot`, `coe_bot`, `unop_bot`, `op_eq_bot`, `bot_prod_bot`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	9 math math: `coe_inf`, `map_comap_eq`, `map_inf`, `comap_inf_map_of_injective`, `map_inf_comap_of_surjective`, `mem_inf`, `comap_inf`, `op_inf`, `unop_inf`
`instPartialOrder` 📖	CompOp	45 math math: `AddSubsemigroup.coe_toSubsemigroup_symm_apply`, `op_le_op_iff`, `map_le_iff_le_comap`, `opEquiv_symm_apply`, `comap_le_comap_iff_of_surjective`, `AddSubsemigroup.coe_toSubsemigroup_apply`, `topologicalClosure_minimal`, `MulArchimedeanClass.subsemigroup_strictAnti`, `AddSubsemigroup.toSubsemigroup'_closure`, `MulHom.mclosure_preimage_le`, `le_comap_of_map_le`, `gc_map_comap`, `closure_le_centralizer_centralizer`, `NonUnitalSubsemiring.toSubsemigroup_strictMono`, `toAddSubsemigroup_closure`, `topologicalClosure_mono`, `closure_le`, `mk_le_mk`, `monotone_comap`, `monotone_map`, `NonUnitalSubsemiring.toSubsemigroup_mono`, `closure_singleton_le_iff_mem`, `map_le_of_le_comap`, `opEquiv_apply`, `Submonoid.mk_le_mk`, `le_comap_map`, `NonUnitalSubring.toSubsemigroup_mono`, `coe_toAddSubsemigroup_symm_apply`, `map_strictMono_of_injective`, `map_comap_le`, `AddSubsemigroup.toSubsemigroup_closure`, `le_op_iff`, `center_le_centralizer`, `unop_le_unop_iff`, `closure_mono`, `prod_mono`, `centralizer_le`, `comap_strictMono_of_surjective`, `le_prod_iff`, `toAddSubsemigroup'_closure`, `NonUnitalSubring.toSubsemigroup_strictMono`, `op_le_iff`, `coe_toAddSubsemigroup_apply`, `map_le_map_iff_of_injective`, `le_topologicalClosure`
`instSetLike` 📖	CompOp	152 math math: `Submonoid.mem_toSubsemigroup`, `coe_inf`, `MulHom.coe_srange`, `Subgroup.centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `AddSubsemigroup.coe_toSubsemigroup_symm_apply`, `MulHom.subsemigroupComap_apply_coe`, `centerCongr_symm_apply_coe`, `mem_sSup_of_mem`, `Subring.centerCongr_apply_coe`, `NonUnitalSubsemiring.centerCongr_symm_apply_coe`, `MulHom.coe_srangeRestrict`, `top_closure_mul_self_subset`, `mul_mem`, `equivOp_symm_apply_coe`, `NonUnitalSubring.centerCongr_apply_coe`, `mem_corner_iff_mem_range_mul_right`, `Subsemiring.centerCongr_symm_apply_coe`, `AddSubsemigroup.coe_toSubsemigroup_apply`, `Submonoid.mk_eq_bot`, `mem_map`, `NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe`, `mem_iSup_prop`, `mul_mem_sup`, `MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top`, `NonUnitalSubring.topEquiv_symm_apply_coe`, `Subgroup.centerCongr_apply_coe`, `notMem_bot`, `coe_prod`, `Submonoid.centerToMulOpposite_apply_coe`, `topEquiv_symm_apply_coe`, `coe_topologicalClosure`, `Submonoid.closure_eq_one_union`, `mem_map_of_mem`, `instMulMemClass`, `Subgroup.centerToMulOpposite_apply_coe`, `MulEquiv.ofLeftInverse_symm_apply`, `coe_centralizer`, `mem_iSup_of_directed`, `mem_sSup_of_directed_on`, `MulEquiv.strictMono_subsemigroupCongr`, `mem_center_iff`, `closure_le_centralizer_centralizer`, `mem_op`, `MulHom.mem_eqLocus`, `Subsemiring.centerCongr_apply_coe`, `mem_mk`, `MulHom.eqOn_closure`, `topEquiv_toMulHom`, `NonUnitalSubring.topEquiv_apply`, `separatelyContinuousMul`, `mem_centralizer_iff`, `Subring.centerToMulOpposite_symm_apply_coe`, `NonUnitalStarAlgebra.adjoin_eq_span`, `MulHom.subsemigroupMap_surjective`, `mem_prod`, `mem_map_iff_mem`, `Subsemiring.centerToMulOpposite_symm_apply_coe`, `mem_biSup_of_directedOn`, `continuousMul`, `coe_sInf`, `nonUnitalSubsemiringClosure_coe`, `NonUnitalSubring.mem_toSubsemigroup`, `instCanLiftSetCoeForallForallForallMemForallHMul`, `closure_le`, `NonUnitalSubring.centerCongr_symm_apply_coe`, `mem_corner_iff`, `Subsemiring.centerToMulOpposite_apply_coe`, `Submonoid.centerToMulOpposite_symm_apply_coe`, `centralizer_eq_top_iff_subset`, `MulEquiv.ofLeftInverse_apply`, `isMulCommutative_closure`, `strictMono_topEquiv`, `coe_unop`, `range_subtype`, `mem_sup_left`, `coe_comap`, `mem_top`, `Submonoid.centerCongr_symm_apply_coe`, `MulHom.mem_srange`, `NonUnitalSubsemiring.closure_subsemigroup_closure`, `Subring.centerToMulOpposite_apply_coe`, `mem_comap`, `centerToMulOpposite_symm_apply_coe`, `Module.End.mem_subsemigroupCenter_iff`, `Submonoid.mem_mk`, `mem_iInf`, `mem_square`, `isClosed_topologicalClosure`, `NonUnitalSubsemiring.coe_toSubsemigroup`, `mem_closure`, `closure_closure_coe_preimage`, `mem_corner_iff_mul_right`, `coe_set_mk`, `eq_top_iff'`, `mem_closure_of_mem`, `closure_singleton_le_iff_mem`, `ext_iff`, `mem_sInf`, `mem_corner_iff_mul_left`, `mem_inf`, `mem_map_equiv`, `mem_iSup_of_mem`, `NonUnitalSubring.centerToMulOpposite_symm_apply_coe`, `subset_closure`, `Subring.centerCongr_symm_apply_coe`, `coe_copy`, `coe_bot`, `coe_toAddSubsemigroup_symm_apply`, `mem_iSup`, `topEquiv_apply`, `mem_unop`, `mem_sup_right`, `closure_eq`, `NonUnitalSubsemiring.centerToMulOpposite_apply_coe`, `instIsMulCommutative_closure`, `NonUnitalSubring.mem_closure_iff`, `coe_iSup_of_directed`, `apply_coe_mem_map`, `MulHom.srangeRestrict_surjective`, `FiniteMulArchimedeanClass.subsemigroup_eq_subgroup`, `MulHom.subsemigroupMap_apply_coe`, `coe_top`, `iSup_eq_closure`, `Submonoid.coe_set_mk`, `NonUnitalSubsemiring.centerCongr_apply_coe`, `coe_op`, `NonUnitalSubring.coe_toSubsemigroup`, `MulEquiv.subsemigroupMap_apply_coe`, `MulEquiv.subsemigroupMap_symm_apply_coe`, `equivOp_apply_coe`, `NonUnitalSubsemiring.mem_closure_iff`, `NonUnitalSubsemiring.mem_toSubsemigroup`, `Submonoid.centerCongr_apply_coe`, `Subgroup.centerToMulOpposite_symm_apply_coe`, `coe_sSup_of_directed_on`, `NonUnitalSubring.centerToMulOpposite_apply_coe`, `nonUnitalSubsemiringClosure_toAddSubmonoid`, `coe_equivMapOfInjective_apply`, `NonUnitalSubsemiring.coe_closure_eq`, `mem_corner_iff_mem_range_mul_left`, `coe_ofClass`, `coe_map`, `nonUnitalSubsemiringClosure_eq_closure`, `mem_carrier`, `coe_iInf`, `centerCongr_apply_coe`, `NonUnitalSubsemiring.topEquiv_symm_apply_coe`, `coe_toAddSubsemigroup_apply`, `NonUnitalAlgebra.adjoin_eq_span`, `NonUnitalSubsemiring.topEquiv_apply`, `coe_square`
`instTop` 📖	CompOp	32 math math: `srange_snd`, `NonUnitalSubring.topEquiv_symm_apply_coe`, `topEquiv_symm_apply_coe`, `MulHom.srange_eq_top_iff_surjective`, `topEquiv_toMulHom`, `NonUnitalSubring.topEquiv_apply`, `op_eq_top`, `centralizer_eq_top_iff_subset`, `strictMono_topEquiv`, `prod_top`, `mem_top`, `srange_fst`, `unop_eq_top`, `MulHom.srange_eq_top_of_surjective`, `top_prod`, `closure_closure_coe_preimage`, `MulHom.srange_eq_map`, `eq_top_iff'`, `center_eq_top`, `topEquiv_apply`, `comap_top`, `map_equiv_top`, `coe_top`, `mk_eq_top`, `prod_eq_top_iff`, `top_prod_top`, `unop_top`, `op_top`, `Submonoid.mk_eq_top`, `NonUnitalSubsemiring.topEquiv_symm_apply_coe`, `closure_univ`, `NonUnitalSubsemiring.topEquiv_apply`
`ofClass` 📖	CompOp	1 math math: `coe_ofClass`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `Subsemigroup` `instSetLike`	`SetLike.coe` `Subsemigroup` `instSetLike` `copy`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_ofClass` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `instSetLike` `ofClass`	—	—
`coe_set_mk` 📖	mathematical	`Set` `Set.instMembership`	`SetLike.coe` `Subsemigroup` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `Subsemigroup` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`Subsemigroup` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike`	—	`ext`
`instCanLiftSetCoeForallForallForallMemForallHMul` 📖	mathematical	—	`CanLift` `Set` `Subsemigroup` `SetLike.coe` `instSetLike`	—	—
`instMulMemClass` 📖	mathematical	—	`MulMemClass` `Subsemigroup` `instSetLike`	—	`mul_mem'`
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `Subsemigroup`	—	`notMem_bot`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `carrier` `Subsemigroup` `SetLike.instMembership` `instSetLike`	—	—
`mem_inf` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_mk` 📖	mathematical	`Set` `Set.instMembership`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership`	—	—
`mem_top` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`mk_eq_bot` 📖	mathematical	`Set` `Set.instMembership`	`Bot.bot` `Subsemigroup` `instBot` `Set` `Set.instEmptyCollection`	—	—
`mk_eq_top` 📖	mathematical	`Set` `Set.instMembership`	`Top.top` `Subsemigroup` `instTop` `Set.univ`	—	—
`mk_le_mk` 📖	mathematical	`Set` `Set.instMembership`	`Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instHasSubset`	—	—
`mul_mem` 📖	mathematical	`Subsemigroup` `SetLike.instMembership` `instSetLike`	`Subsemigroup` `SetLike.instMembership` `instSetLike`	—	`mul_mem'`
`mul_mem'` 📖	mathematical	`Set` `Set.instMembership` `carrier`	`Set` `Set.instMembership` `carrier`	—	—
`notMem_bot` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`Set.notMem_empty`
`subsingleton_of_subsingleton` 📖	—	—	—	—	`notMem_bot`

(root)

Definitions

Name	Category	Theorems
`AddMemClass` 📖	CompData	3 math math: `AddSubmonoidClass.toAddMemClass`, `AddSubsemigroup.instAddMemClass`, `ConvexCone.instAddMemClass`
`AddSubsemigroup` 📖	CompData	212 math math: `AddSubgroup.centerToAddOpposite_apply_coe`, `ArchimedeanClass.subsemigroup_eq_addSubgroup_of_ne_top`, `AddSubsemigroup.closure_iUnion`, `AddSubsemigroup.add_mem`, `AddSubsemigroup.op_iSup`, `AddSubsemigroup.closure_le_centralizer_centralizer`, `AddHom.coe_srangeRestrict`, `AddHom.subsemigroupMap_apply_coe`, `AddSubsemigroup.mem_closure`, `AddSubsemigroup.coe_toSubsemigroup_symm_apply`, `AddSubsemigroup.map_inf_comap_of_surjective`, `AddSubsemigroup.center_eq_top`, `AddSubsemigroup.coe_inf`, `AddSubsemigroup.closure_univ`, `AddSubsemigroup.comap_injective_of_surjective`, `AddSubsemigroup.prod_eq_top_iff`, `AddSubsemigroup.op_eq_top`, `AddSubsemigroup.unop_iInf`, `AddSubsemigroup.comap_iInf`, `AddHom.srangeRestrict_surjective`, `AddSubsemigroup.le_op_iff`, `AddSubsemigroup.mem_map_equiv`, `AddSubsemigroup.coe_toSubsemigroup_apply`, `AddSubsemigroup.center_le_centralizer`, `AddSubsemigroup.coe_iSup_of_directed`, `AddHom.subsemigroupMap_surjective`, `AddSubsemigroup.op_le_iff`, `AddSubsemigroup.mem_centralizer_iff`, `AddSubsemigroup.map_sup`, `AddSubsemigroup.notMem_bot`, `AddSubsemigroup.unop_sSup`, `AddSubmonoid.centerCongr_symm_apply_coe`, `AddSubsemigroup.coe_top`, `AddSubsemigroup.coe_prod`, `AddSubsemigroup.unop_iSup`, `AddSubsemigroup.coe_bot`, `AddSubsemigroup.toSubsemigroup'_closure`, `AddHom.srange_eq_top_of_surjective`, `AddSubsemigroup.map_le_map_iff_of_injective`, `AddSubsemigroup.topEquiv_apply`, `AddSubsemigroup.map_iSup`, `AddSubsemigroup.op_top`, `AddSubsemigroup.mem_closure_of_mem`, `AddSubsemigroup.op_eq_bot`, `AddSubmonoid.centerToAddOpposite_symm_apply_coe`, `AddSubsemigroup.map_injective_of_injective`, `AddSubsemigroup.mem_unop`, `AddSubsemigroup.centerToAddOpposite_symm_apply_coe`, `AddHom.eqOn_closure`, `AddSubsemigroup.mem_center_iff`, `AddSubsemigroup.unop_eq_bot`, `AddSubsemigroup.mem_iSup`, `AddSubsemigroup.mem_map_of_mem`, `AddSubsemigroup.mem_biSup_of_directedOn`, `AddSubsemigroup.continuousAdd`, `AddSubsemigroup.mem_mk`, `AddSubsemigroup.centralizer_le`, `AddHom.srange_eq_top_iff_surjective`, `AddSubsemigroup.comap_inf`, `AddSubsemigroup.map_bot`, `AddSubsemigroup.coe_sumNonzeroSq`, `AddSubsemigroup.comap_sup_map_of_injective`, `AddSubsemigroup.mem_sup_left`, `AddSubsemigroup.le_comap_map`, `AddSubsemigroup.srange_snd`, `AddSubsemigroup.mem_prod`, `AddSubsemigroup.op_iInf`, `AddSubsemigroup.op_sInf`, `AddEquiv.ofLeftInverse_apply`, `AddSubsemigroup.unop_sup`, `AddSubsemigroup.le_prod_iff`, `AddSubsemigroup.opEquiv_symm_apply`, `AddSubsemigroup.map_comap_eq`, `AddSubsemigroup.topEquiv_symm_apply_coe`, `AddSubsemigroup.instAddMemClass`, `AddSubgroup.centerCongr_apply_coe`, `AddEquiv.subsemigroupMap_apply_coe`, `AddSubsemigroup.mem_iSup_of_mem`, `AddSubsemigroup.subset_closure`, `AddSubsemigroup.centerCongr_apply_coe`, `AddSubsemigroup.topologicalClosure_minimal`, `AddSubsemigroup.top_prod_top`, `AddSubsemigroup.op_le_op_iff`, `AddSubsemigroup.instCanLiftSetCoeForallForallForallMemForallHAdd`, `AddSubsemigroup.mem_carrier`, `Subsemigroup.toAddSubsemigroup_closure`, `AddSubsemigroup.closure_closure_coe_preimage`, `AddSubsemigroup.op_sup`, `AddSubsemigroup.coe_map`, `AddSubsemigroup.mem_iInf`, `AddSubsemigroup.isAddCommutative_closure`, `AddSubsemigroup.closure_eq`, `FiniteArchimedeanClass.subsemigroup_eq_addSubgroup`, `AddSubsemigroup.coe_sInf`, `AddSubsemigroup.comap_inf_map_of_injective`, `AddSubsemigroup.op_sSup`, `AddSubsemigroup.unop_sInf`, `AddSubsemigroup.strictMono_topEquiv`, `AddHom.srange_eq_map`, `AddSubsemigroup.map_iInf_comap_of_surjective`, `AddSubsemigroup.closure_singleton_le_iff_mem`, `AddSubsemigroup.mem_sInf`, `AddSubsemigroup.bot_prod_bot`, `AddEquiv.strictMono_subsemigroupCongr`, `AddSubsemigroup.comap_iSup_map_of_injective`, `AddSubsemigroup.map_equiv_top`, `AddSubsemigroup.coe_equivMapOfInjective_apply`, `AddSubsemigroup.iSup_eq_closure`, `AddSubsemigroup.comap_strictMono_of_surjective`, `AddSubsemigroup.unop_injective`, `AddSubgroup.centerCongr_symm_apply_coe`, `ArchimedeanClass.subsemigroup_strictAnti`, `AddSubsemigroup.range_subtype`, `AddSubsemigroup.coe_unop`, `AddSubsemigroup.closure_le`, `AddSubsemigroup.mem_top`, `AddSubsemigroup.topologicalClosure_mono`, `AddSubsemigroup.coe_topologicalClosure`, `AddSubsemigroup.unop_top`, `AddSubsemigroup.comap_iInf_map_of_injective`, `AddSubsemigroup.mem_sup_right`, `AddSubsemigroup.centralizer_eq_top_iff_subset`, `AddSubsemigroup.map_iSup_comap_of_surjective`, `AddSubsemigroup.op_injective`, `AddSubsemigroup.unop_bot`, `AddSubsemigroup.mem_comap`, `AddSubsemigroup.centerCongr_symm_apply_coe`, `AddSubsemigroup.eq_top_iff'`, `AddSubsemigroup.mem_map`, `AddSubsemigroup.unop_inf`, `AddSubmonoid.mem_mk`, `AddSubsemigroup.equivOp_symm_apply_coe`, `AddSubsemigroup.mem_sumNonzeroSq`, `AddSubsemigroup.mem_op`, `AddSubsemigroup.comap_top`, `AddSubsemigroup.map_comap_le`, `AddSubsemigroup.le_comap_of_map_le`, `AddSubsemigroup.mk_le_mk`, `AddSubsemigroup.coe_centralizer`, `AddSubsemigroup.unop_le_unop_iff`, `AddSubsemigroup.monotone_comap`, `AddSubsemigroup.mem_sSup_of_mem`, `AddSubgroup.centerToAddOpposite_symm_apply_coe`, `AddSubmonoid.centerCongr_apply_coe`, `AddSubsemigroup.top_prod`, `AddSubsemigroup.mk_eq_top`, `Subsemigroup.coe_toAddSubsemigroup_symm_apply`, `AddSubsemigroup.map_surjective_of_surjective`, `AddSubmonoid.mk_eq_top`, `AddSubsemigroup.op_bot`, `AddSubsemigroup.map_sup_comap_of_surjective`, `AddSubsemigroup.mem_inf`, `AddHom.subsemigroupComap_apply_coe`, `AddSubsemigroup.coe_comap`, `AddSubsemigroup.mem_iSup_prop`, `AddSubsemigroup.mem_map_iff_mem`, `AddSubsemigroup.prod_mono`, `AddSubmonoid.mk_le_mk`, `AddSubsemigroup.map_le_iff_le_comap`, `AddSubsemigroup.mem_sSup_of_directed_on`, `AddSubsemigroup.coe_sSup_of_directed_on`, `AddSubsemigroup.closure_union`, `AddEquiv.subsemigroupMap_symm_apply_coe`, `AddSubsemigroup.top_closure_add_self_subset`, `AddSubsemigroup.map_strictMono_of_injective`, `AddSubsemigroup.topEquiv_toAddHom`, `AddSubsemigroup.coe_set_mk`, `AddSubsemigroup.toSubsemigroup_closure`, `AddSubsemigroup.comap_le_comap_iff_of_surjective`, `AddSubsemigroup.add_mem_sup`, `AddSubsemigroup.opEquiv_apply`, `AddSubsemigroup.mem_iSup_of_directed`, `AddSubsemigroup.separatelyContinuousAdd`, `AddHom.mem_eqLocus`, `AddSubsemigroup.map_inf`, `AddSubsemigroup.equivOp_apply_coe`, `AddSubsemigroup.mk_eq_bot`, `AddHom.mclosure_preimage_le`, `AddSubsemigroup.closure_mono`, `AddSubsemigroup.isClosed_topologicalClosure`, `AddSubsemigroup.monotone_map`, `AddSubsemigroup.map_iInf`, `AddSubsemigroup.srange_fst`, `AddHom.mem_srange`, `AddSubsemigroup.coe_iInf`, `AddSubsemigroup.closure_empty`, `AddSubsemigroup.instNontrivialOfNonempty`, `AddSubsemigroup.centerToAddOpposite_apply_coe`, `AddSubsemigroup.mem_even`, `AddSubsemigroup.apply_coe_mem_map`, `AddSubsemigroup.ext_iff`, `AddSubsemigroup.coe_ofClass`, `AddSubsemigroup.op_inf`, `AddSubsemigroup.coe_even`, `Subsemigroup.toAddSubsemigroup'_closure`, `AddSubmonoid.coe_set_mk`, `AddSubsemigroup.le_topologicalClosure`, `AddSubsemigroup.comap_surjective_of_injective`, `AddSubsemigroup.instIsAddCommutative_closure`, `AddEquiv.ofLeftInverse_symm_apply`, `AddSubsemigroup.map_le_of_le_comap`, `AddSubmonoid.mem_toSubsemigroup`, `AddSubsemigroup.coe_op`, `AddHom.coe_srange`, `AddSubsemigroup.gc_map_comap`, `AddSubmonoid.toSubsemigroup_injective`, `AddSubsemigroup.prod_top`, `Subsemigroup.coe_toAddSubsemigroup_apply`, `AddSubmonoid.centerToAddOpposite_apply_coe`, `AddSubsemigroup.coe_copy`, `AddSubmonoid.mk_eq_bot`, `AddSubsemigroup.unop_eq_top`
`MulMemClass` 📖	CompData	3 math math: `Subsemigroup.instMulMemClass`, `SubmonoidClass.toMulMemClass`, `NonUnitalSubsemiringClass.mulMemClass`
`Subsemigroup` 📖	CompData	258 math math: `Subsemigroup.map_iInf_comap_of_surjective`, `Submonoid.mem_toSubsemigroup`, `Subsemigroup.coe_inf`, `Subsemigroup.srange_snd`, `MulHom.coe_srange`, `Subgroup.centerCongr_symm_apply_coe`, `Subsemigroup.unop_iSup`, `Subsemigroup.centerToMulOpposite_apply_coe`, `AddSubsemigroup.coe_toSubsemigroup_symm_apply`, `MulHom.subsemigroupComap_apply_coe`, `Subsemigroup.centerCongr_symm_apply_coe`, `Subsemigroup.op_le_op_iff`, `Subsemigroup.map_le_iff_le_comap`, `Subsemigroup.mem_sSup_of_mem`, `Subsemigroup.opEquiv_symm_apply`, `Subring.centerCongr_apply_coe`, `NonUnitalSubsemiring.centerCongr_symm_apply_coe`, `Subsemigroup.comap_le_comap_iff_of_surjective`, `MulHom.coe_srangeRestrict`, `Subsemigroup.top_closure_mul_self_subset`, `Subsemigroup.mul_mem`, `Subsemigroup.equivOp_symm_apply_coe`, `NonUnitalSubring.centerCongr_apply_coe`, `Subsemigroup.mem_corner_iff_mem_range_mul_right`, `Subsemiring.centerCongr_symm_apply_coe`, `AddSubsemigroup.coe_toSubsemigroup_apply`, `Subsemigroup.comap_injective_of_surjective`, `Submonoid.mk_eq_bot`, `Subsemigroup.mem_map`, `Subsemigroup.topologicalClosure_minimal`, `NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe`, `Subsemigroup.mem_iSup_prop`, `Subsemigroup.mul_mem_sup`, `MulArchimedeanClass.subsemigroup_strictAnti`, `MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top`, `AddSubsemigroup.toSubsemigroup'_closure`, `MulHom.mclosure_preimage_le`, `Subsemigroup.closure_empty`, `NonUnitalSubring.topEquiv_symm_apply_coe`, `Subsemigroup.le_comap_of_map_le`, `Subgroup.centerCongr_apply_coe`, `Subsemigroup.notMem_bot`, `Subsemigroup.coe_prod`, `Submonoid.centerToMulOpposite_apply_coe`, `Subsemigroup.topEquiv_symm_apply_coe`, `Subsemigroup.unop_eq_bot`, `Subsemigroup.coe_topologicalClosure`, `Submonoid.closure_eq_one_union`, `Subsemigroup.mem_map_of_mem`, `Subsemigroup.instMulMemClass`, `Subgroup.centerToMulOpposite_apply_coe`, `MulEquiv.ofLeftInverse_symm_apply`, `Subsemigroup.gc_map_comap`, `Subsemigroup.coe_centralizer`, `Subsemigroup.mem_iSup_of_directed`, `Subsemigroup.mem_sSup_of_directed_on`, `Subsemigroup.map_sup`, `MulEquiv.strictMono_subsemigroupCongr`, `Subsemigroup.mem_center_iff`, `MulHom.srange_eq_top_iff_surjective`, `Subsemigroup.closure_le_centralizer_centralizer`, `Subsemigroup.mem_op`, `MulHom.mem_eqLocus`, `Subsemiring.centerCongr_apply_coe`, `Subsemigroup.mem_mk`, `MulHom.eqOn_closure`, `NonUnitalSubsemiring.toSubsemigroup_strictMono`, `Subsemigroup.topEquiv_toMulHom`, `NonUnitalSubring.topEquiv_apply`, `Subsemigroup.separatelyContinuousMul`, `Subsemigroup.mem_centralizer_iff`, `Subring.centerToMulOpposite_symm_apply_coe`, `NonUnitalStarAlgebra.adjoin_eq_span`, `MulHom.subsemigroupMap_surjective`, `Subsemigroup.toAddSubsemigroup_closure`, `Subsemigroup.mem_prod`, `Subsemigroup.op_iInf`, `Subsemigroup.topologicalClosure_mono`, `Subsemigroup.mem_map_iff_mem`, `Subsemiring.centerToMulOpposite_symm_apply_coe`, `Subsemigroup.mem_biSup_of_directedOn`, `Subsemigroup.continuousMul`, `Subsemigroup.coe_sInf`, `Submonoid.toSubsemigroup_injective`, `Subsemigroup.nonUnitalSubsemiringClosure_coe`, `NonUnitalSubring.mem_toSubsemigroup`, `Subsemigroup.instCanLiftSetCoeForallForallForallMemForallHMul`, `Subsemigroup.map_comap_eq`, `Subsemigroup.closure_le`, `NonUnitalSubring.centerCongr_symm_apply_coe`, `Subsemigroup.mem_corner_iff`, `Subsemiring.centerToMulOpposite_apply_coe`, `Subsemigroup.closure_union`, `Subsemigroup.unop_sup`, `Subsemigroup.comap_sup_map_of_injective`, `Subsemigroup.comap_iSup_map_of_injective`, `Subsemigroup.op_eq_top`, `Submonoid.centerToMulOpposite_symm_apply_coe`, `Subsemigroup.centralizer_eq_top_iff_subset`, `MulEquiv.ofLeftInverse_apply`, `Subsemigroup.isMulCommutative_closure`, `Subsemigroup.strictMono_topEquiv`, `Subsemigroup.coe_unop`, `NonUnitalSubring.sInf_toSubsemigroup`, `Subsemigroup.map_inf`, `Subsemigroup.prod_top`, `NonUnitalSubring.toSubsemigroup_injective`, `Subsemigroup.range_subtype`, `Subsemigroup.mem_sup_left`, `Subsemigroup.coe_comap`, `Subsemigroup.mem_top`, `Subsemigroup.srange_fst`, `Subsemigroup.unop_injective`, `Subsemigroup.op_sup`, `Submonoid.centerCongr_symm_apply_coe`, `MulHom.mem_srange`, `Subsemigroup.comap_inf_map_of_injective`, `Subsemigroup.instNontrivialOfNonempty`, `NonUnitalSubsemiring.closure_subsemigroup_closure`, `Subring.centerToMulOpposite_apply_coe`, `Subsemigroup.comap_iInf_map_of_injective`, `Subsemigroup.unop_eq_top`, `Subsemigroup.mk_le_mk`, `Subsemigroup.monotone_comap`, `Subsemigroup.mem_comap`, `Subsemigroup.centerToMulOpposite_symm_apply_coe`, `MulHom.srange_eq_top_of_surjective`, `Subsemigroup.mk_eq_bot`, `Module.End.mem_subsemigroupCenter_iff`, `Submonoid.mem_mk`, `Subsemigroup.mem_iInf`, `Subsemigroup.monotone_map`, `Subsemigroup.mem_square`, `Subsemigroup.isClosed_topologicalClosure`, `NonUnitalSubsemiring.coe_toSubsemigroup`, `Subsemigroup.mem_closure`, `Subsemigroup.top_prod`, `Subsemigroup.map_inf_comap_of_surjective`, `Subsemigroup.closure_closure_coe_preimage`, `Subsemigroup.op_iSup`, `Subsemigroup.mem_corner_iff_mul_right`, `Subsemigroup.map_iInf`, `Subsemigroup.coe_set_mk`, `Subsemigroup.op_bot`, `MulHom.srange_eq_map`, `NonUnitalSubsemiring.toSubsemigroup_mono`, `Subsemigroup.eq_top_iff'`, `Subsemigroup.mem_closure_of_mem`, `Subsemigroup.closure_singleton_le_iff_mem`, `Subsemigroup.ext_iff`, `Subsemigroup.map_le_of_le_comap`, `Subsemigroup.mem_sInf`, `Subsemigroup.closure_iUnion`, `Subsemigroup.mem_corner_iff_mul_left`, `Subsemigroup.mem_inf`, `Subsemigroup.opEquiv_apply`, `Subsemigroup.mem_map_equiv`, `Subsemigroup.mem_iSup_of_mem`, `Submonoid.mk_le_mk`, `Subsemigroup.map_bot`, `NonUnitalSubring.centerToMulOpposite_symm_apply_coe`, `Subsemigroup.subset_closure`, `Subring.centerCongr_symm_apply_coe`, `Subsemigroup.coe_copy`, `Subsemigroup.le_comap_map`, `Subsemigroup.coe_bot`, `NonUnitalSubring.toSubsemigroup_mono`, `Subsemigroup.op_sInf`, `Subsemigroup.center_eq_top`, `Subsemigroup.coe_toAddSubsemigroup_symm_apply`, `Subsemigroup.mem_iSup`, `Subsemigroup.topEquiv_apply`, `Subsemigroup.unop_sInf`, `Subsemigroup.mem_unop`, `Subsemigroup.mem_sup_right`, `Subsemigroup.comap_top`, `Subsemigroup.map_strictMono_of_injective`, `Subsemigroup.map_surjective_of_surjective`, `Subsemigroup.closure_eq`, `NonUnitalSubsemiring.toSubsemigroup_injective`, `Subsemigroup.unop_bot`, `NonUnitalSubsemiring.centerToMulOpposite_apply_coe`, `Subsemigroup.instIsMulCommutative_closure`, `Subsemigroup.map_comap_le`, `NonUnitalSubring.mem_closure_iff`, `Subsemigroup.map_iSup`, `Subsemigroup.map_injective_of_injective`, `Subsemigroup.map_iSup_comap_of_surjective`, `Subsemigroup.coe_iSup_of_directed`, `Subsemigroup.apply_coe_mem_map`, `MulHom.srangeRestrict_surjective`, `FiniteMulArchimedeanClass.subsemigroup_eq_subgroup`, `Subsemigroup.map_equiv_top`, `MulHom.subsemigroupMap_apply_coe`, `NonUnitalSubsemiring.sInf_toSubsemigroup`, `Subsemigroup.op_eq_bot`, `AddSubsemigroup.toSubsemigroup_closure`, `Subsemigroup.coe_top`, `Subsemigroup.bot_prod_bot`, `Subsemigroup.unop_iInf`, `Subsemigroup.mk_eq_top`, `Subsemigroup.le_op_iff`, `Subsemigroup.center_le_centralizer`, `Subsemigroup.prod_eq_top_iff`, `Subsemigroup.comap_inf`, `Subsemigroup.comap_surjective_of_injective`, `Subsemigroup.unop_le_unop_iff`, `Subsemigroup.iSup_eq_closure`, `Submonoid.coe_set_mk`, `NonUnitalSubsemiring.centerCongr_apply_coe`, `Subsemigroup.closure_mono`, `Subsemigroup.coe_op`, `Subsemigroup.op_inf`, `NonUnitalSubring.coe_toSubsemigroup`, `MulEquiv.subsemigroupMap_apply_coe`, `MulEquiv.subsemigroupMap_symm_apply_coe`, `Subsemigroup.op_injective`, `Subsemigroup.equivOp_apply_coe`, `Subsemigroup.prod_mono`, `Subsemigroup.centralizer_le`, `NonUnitalSubsemiring.mem_closure_iff`, `NonUnitalSubsemiring.mem_toSubsemigroup`, `Subsemigroup.map_sup_comap_of_surjective`, `Submonoid.centerCongr_apply_coe`, `Subsemigroup.comap_strictMono_of_surjective`, `Subgroup.centerToMulOpposite_symm_apply_coe`, `Subsemigroup.coe_sSup_of_directed_on`, `Subsemigroup.top_prod_top`, `Subsemigroup.unop_sSup`, `Subsemigroup.le_prod_iff`, `Subsemigroup.op_sSup`, `NonUnitalSubring.centerToMulOpposite_apply_coe`, `Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid`, `Subsemigroup.coe_equivMapOfInjective_apply`, `NonUnitalSubsemiring.coe_closure_eq`, `Subsemigroup.mem_corner_iff_mem_range_mul_left`, `Subsemigroup.toAddSubsemigroup'_closure`, `Subsemigroup.unop_top`, `Subsemigroup.op_top`, `Subsemigroup.coe_ofClass`, `NonUnitalSubring.toSubsemigroup_strictMono`, `Submonoid.mk_eq_top`, `Subsemigroup.coe_map`, `Subsemigroup.nonUnitalSubsemiringClosure_eq_closure`, `Subsemigroup.unop_inf`, `Subsemigroup.mem_carrier`, `Subsemigroup.coe_iInf`, `Subsemigroup.centerCongr_apply_coe`, `Subsemigroup.op_le_iff`, `NonUnitalSubsemiring.topEquiv_symm_apply_coe`, `Subsemigroup.coe_toAddSubsemigroup_apply`, `Subsemigroup.closure_univ`, `NonUnitalAlgebra.adjoin_eq_span`, `NonUnitalSubsemiring.topEquiv_apply`, `Subsemigroup.map_le_map_iff_of_injective`, `Subsemigroup.coe_square`, `Subsemigroup.comap_iInf`, `Subsemigroup.le_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddCommutative_iff_of_setLike` 📖	mathematical	—	`IsAddCommutative` `SetLike.instMembership` `AddMemClass.add`	—	`isAddCommutative_iff` `AddMemClass.add_mem`
`isMulCommutative_iff_of_setLike` 📖	mathematical	—	`IsMulCommutative` `SetLike.instMembership` `MulMemClass.mul`	—	`MulMemClass.mul_mem`
`setLike_add_comm` 📖	—	`SetLike.instMembership`	—	—	`isAddCommutative_iff_of_setLike`
`setLike_mul_comm` 📖	—	`SetLike.instMembership`	—	—	`isMulCommutative_iff_of_setLike`

---

← Back to Index