Structures · Algebra
ZeroMemClass
ZeroMemClass S M says S is a type of subsets s ≤ M, such that 0 ∈ s for all s.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Shape
- 2 explicit arguments · adds zero_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
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 by29
- ZeroMemClass.zero_mem
- RestrictedProduct.single
- ZeroMemClass.coe_zero
- ZeroMemClass.coe_eq_zero
- RestrictedProduct.single_eq_of_ne'
- ZeroMemClass.coe_nonempty
- RestrictedProduct.single_injective
- Set.injOn_iff_map_eq_zero
- RestrictedProduct.comp_single
- RestrictedProduct.single_ne_zero_iff
- MulZeroMemClass.isRightCancelMulZero
- RestrictedProduct.coe_single_apply
- RestrictedProduct.instZeroCoeOfZeroMemClass
- RestrictedProduct.nhds_zero_eq_map_structureMap
- RestrictedProduct.single_inj
- RestrictedProduct.single_eq_same
- RestrictedProduct.single_eq_of_ne
- ZeroMemClass.zero
- MulZeroMemClass.isLeftCancelMulZero
- RestrictedProduct.single.congr_simp
- RestrictedProduct.single_add
- RestrictedProduct.nhds_zero_eq_map_ofPre
- RestrictedProduct.single_zero
- MulZeroMemClass.isCancelMulZero
- RestrictedProduct.zero_apply
- RestrictedProduct.mul_single
- RestrictedProduct.single_eq_zero_iff
- ZeroMemClass.zero_def
- RestrictedProduct.single_mul
Ancestors0
No ancestors.