Structures · Algebra
AddMemClass
AddMemClass S M says S is a type of sets s : Set M that are closed under (+)
- Defined in
- Mathlib.Algebra.Group.Subsemigroup.Defs
- Shape
- 2 explicit arguments · adds add_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- ConvexCone
- AddSubsemigroup
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- AddMemClass.add_mem
- IsAddCommutative.of_setLike_add_comm
- setLike_add_comm
- AddMemClass.subtype
- AddMemClass.mk_add_mk
- AddHom.domRestrict
- isAddCommutative_iff_of_setLike
- AddHom.codRestrict
- Set.injOn_iff_map_eq_zero
- AddSubsemigroup.ofClass
- AddHom.domRestrict_apply
- AddSubsemigroup.instIsAddCommutative_closure
- AddMemClass.toAddCommSemigroup
- RestrictedProduct.add_apply
- RestrictedProduct.instContinuousAddCoeCofinite
- AddMemClass.isLeftCancelAdd
- AddMemClass.isRightCancelAdd
- AddSubsemigroup.coe_ofClass
- AddHom.codRestrict_apply_coe
- AddHom.restrict_apply
- RestrictedProduct.instContinuousAddCoePrincipal
- AddMemClass.add
- AddHom.restrict
- AddMemClass.subtype_apply
- AddMemClass.toAddSemigroup
- AddMemClass.coe_add
- AddSubgroup.instIsAddCommutative_closure
- RestrictedProduct.instAddCoeOfAddMemClass
- RestrictedProduct.single_add
- AddMemClass.coe_subtype
- AddMemClass.isCancelAdd
- AddSubmonoid.instIsAddCommutative_closure
- AddMemClass.add_def
- AddMemClass.subtype_injective
Ancestors0
No ancestors.