Open tonyxty opened 3 years ago
Subsets are currently only defined for Monoids: https://github.com/JetBrains/arend-lib/blob/6be71a0b2477906448d873f07277ec3289b31796/src/Algebra/Ring/Localization.ard#L23-L32 while they can be defined for BaseSets. It goes without saying that this is useful in general.
Subset
Monoid
BaseSet
Subsets are currently only defined forMonoids: https://github.com/JetBrains/arend-lib/blob/6be71a0b2477906448d873f07277ec3289b31796/src/Algebra/Ring/Localization.ard#L23-L32 while they can be defined forBaseSets. It goes without saying that this is useful in general.