Structures · Algebra
OneMemClass
OneMemClass S M says S is a type of subsets s ≤ M, such that 1 ∈ s for all s.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Shape
- 2 explicit arguments · adds one_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- OneMemClass.one_mem
- algebraMap_mem
- RestrictedProduct.mulSingle
- OneMemClass.coe_one
- OneMemClass.coe_eq_one
- RestrictedProduct.mulSingle_injective
- RestrictedProduct.comp_mulSingle
- ContinuousMap.AlgHom.closure_ker_inter
- OneMemClass.coe_nonempty
- RestrictedProduct.mulSingle.congr_simp
- RestrictedProduct.mulSingle_eq_of_ne'
- RestrictedProduct.one_apply
- OneMemClass.one_def
- RestrictedProduct.mulSingle_one
- RestrictedProduct.mulSingle_eq_one_iff
- RestrictedProduct.mulSingle_eq_of_ne
- RestrictedProduct.mulSingle_eq_same
- RestrictedProduct.coe_mulSingle_apply
- OneMemClass.one
- RestrictedProduct.mulSingle_mul
- RestrictedProduct.instOneCoeOfOneMemClass
- RestrictedProduct.mulSingle_ne_one_iff
- Set.injOn_iff_map_eq_one
- RestrictedProduct.mulSingle_inj
Ancestors0
No ancestors.