has_mem for subgroup of units

Stream: Is there code for X?

[Adam Topaz]

I think I asked about this before, but it came up again. Do we have something like this instance?

import algebra
import group_theory.subgroup

instance has_mem_unit_subgroup {A : Type*} [monoid A] : has_mem A (subgroup (units A)) :=
⟨ λ x H, x ∈ (coe : units A → A) '' H ⟩

If not, should I add it somewhere?

[Adam Topaz]

Hmmm... also, why does this fail?

import algebra
import group_theory.subgroup
instance has_mem_unit_subgroup' {A : Type*} [monoid A] : has_mem (units A) (subgroup (units A)) := by apply_instance -- FAILS

[Kevin Buzzard]

Works for me! Dirty mathlib?

[Bhavik Mehta]

It might fail in the presence of has_mem_unit_subgroup though because of the out_param in has_mem

[Adam Topaz]

Yeah, it's the out_param that's causing the problem. So there is no way to have has_mem A B and has_mem A' B at the same time?!

[Bhavik Mehta]

Yeah, as far as I know

[Adam Topaz]

Do you have any suggestions for making things like subgroup (units A) not completely awful to work with?

[Bhavik Mehta]

I've never tried to work with it, so I don't have anything helpful to say, sorry!