Structures · Algebra
SDiv
Type class for the /ₛ notation.
- Defined in
- Mathlib.Algebra.Notation.Defs
- Shape
- 2 explicit arguments · adds sdiv
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Set
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- SDiv.sdiv
- Set.singleton_sdiv_singleton
- Set.sdiv_subset_sdiv
- Set.inter_sdiv_union_subset_union
- Set.image2_sdiv
- Set.sdiv_empty
- Set.image_sdiv_prod
- Set.sdiv_union
- Set.sdiv_singleton
- Set.union_sdiv_inter_subset_union
- Function.Surjective.torsor
- Set.singleton_sdiv
- Set.sdiv_inter_subset
- Set.empty_sdiv
- Set.sdiv_subset_sdiv_left
- Set.sdiv_subset_sdiv_right
- Set.sdiv_nonempty
- Set.Nonempty.of_sdiv_left
- Set.Nonempty.sdiv
- Set.sdiv_self_mono
- Set.inter_sdiv_subset
- Function.Injective.torsor
- Set.sdiv_mem_sdiv
- Set.union_sdiv
- Set.sdiv_subset_iff
- Set.sdiv
- Set.sdiv_eq_empty
- Set.mem_sdiv
- Set.Nonempty.of_sdiv_right
Ancestors0
No ancestors.