has_mem for subgroups of units

Stream: Is there code for X?

[Adam Topaz]

Is this instance missing from mathlib?

import algebra

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

[Adam Topaz]

Should it even be an instance?

[Reid Barton]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

I agree. What about the out_param thing?

[Adam Topaz]

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