Structures · Algebra
MulMemClass
MulMemClass 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 mul_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Subsemigroup
How is a type an instance?
Loading the hierarchy index…
Assumed by56
- MulMemClass.mul_mem
- IsMulCommutative.of_setLike_mul_comm
- setLike_mul_comm
- MulMemClass.subtype
- isMulCommutative_iff_of_setLike
- MulHom.domRestrict
- mul_neg_mem
- MulMemClass.mul_mem_add_closure
- MulMemClass.coe_mul
- MulMemClass.mul_right_mem_add_closure
- MulHom.domRestrict_apply
- MulHom.codRestrict
- Subsemigroup.ofClass
- MulMemClass.mul_def
- Subsemigroup.coe_ofClass
- MulMemClass.subtype_injective
- SetLike.instSMulCommClass
- MulZeroMemClass.isRightCancelMulZero
- MulHom.restrict_apply
- Algebra.instIsMulCommutative_adjoin
- MulMemClass.mk_mul_mk
- MulMemClass.isRightCancelMul
- Subsemiring.instIsMulCommutative_closure
- RestrictedProduct.instMulCoeOfMulMemClass
- NonUnitalStarAlgebra.instIsMulCommutative_adjoin
- SetLike.instIsScalarTower
- MulMemClass.coe_subtype
- neg_mul_mem
- Submonoid.instIsMulCommutative_closure
- MulMemClass.isLeftCancelMul
- RestrictedProduct.instContinuousMulCoePrincipal
- MulMemClass.mul_left_mem_add_closure
- MulMemClass.mul
- MulMemClass.subtype_apply
- MulMemClass.isCancelMul
- Subring.instIsMulCommutative_closure
- MulZeroMemClass.isLeftCancelMulZero
- RestrictedProduct.instContinuousMulCoeCofinite
- MulZeroMemClass.isCancelMulZero
- RestrictedProduct.mulSingle_mul
- MulHom.restrict
- StarAlgebra.instIsMulCommutative_adjoin
- MulHom.codRestrict_apply_coe
- NonUnitalAlgebra.instIsMulCommutative_adjoin
- RestrictedProduct.mul_single
- Submonoid.commute_coe_coe
- NonUnitalSubsemiring.instIsMulCommutative_closure
- MulMemClass.toCommSemigroup
- Set.injOn_iff_map_eq_one
- RestrictedProduct.mul_apply
Ancestors0
No ancestors.