## Stream: Is there code for X?

### Topic: has_mem for subgroups of units

#### Adam Topaz (Aug 27 2020 at 13:55):

Is this instance missing from mathlib?

import algebra

variables {A : Type*} [semiring A]
example : has_mem A (subgroup (units A)) := sorry


#### Adam Topaz (Aug 27 2020 at 14:06):

Should it even be an instance?

#### Reid Barton (Aug 27 2020 at 14:15):

isn't it also a bit more tricky to define than one would think

#### Adam Topaz (Aug 27 2020 at 14:19):

example : has_mem A (subgroup (units A)) := ⟨λ a H, a ∈ units.val '' H.carrier⟩


#### Adam Topaz (Aug 27 2020 at 14:21):

Or maybe this is better:

example : has_mem A (subgroup (units A)) :=
⟨λ a H, a ∈ (λ (a : units A), (a : A)) '' (H : set (units A))⟩


#### Adam Topaz (Aug 27 2020 at 15:36):

Well... looking around zulip, it seems that this would cause out_param issues :(

#### Adam Topaz (Aug 27 2020 at 15:39):

But I think this might be safe:

import algebra

variables (A : Type*) [semiring A]
def mult_subgroup := subgroup (units A)

namespace mult_subgroup
instance : has_coe (mult_subgroup A) (set A) := ⟨λ H, coe '' H.carrier⟩
instance : has_mem A (mult_subgroup A) := ⟨λ a H, a ∈ (H : set A)⟩
end mult_subgroup


@Mario Carneiro @Reid Barton Can you confirm?

#### Mario Carneiro (Aug 27 2020 at 19:52):

I think the mult_subgroup is going to obscure the underlying subgroup, meaning that you need a whole bunch of duplicate api

#### Adam Topaz (Aug 27 2020 at 19:56):

I agree. What about the out_param thing?

#### Adam Topaz (Aug 27 2020 at 19:57):

Is there any safe way to define/write a \in H where a : A and H : subgroup (units A)?

Last updated: May 17 2021 at 15:13 UTC