## Stream: Is there code for X?

### Topic: has_mem for subgroup of units

#### Adam Topaz (Nov 23 2020 at 15:39):

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 (Nov 23 2020 at 15:47):

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 (Nov 23 2020 at 16:07):

Works for me! Dirty mathlib?

#### Bhavik Mehta (Nov 23 2020 at 16:14):

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

#### Adam Topaz (Nov 23 2020 at 16:20):

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 (Nov 23 2020 at 16:21):

Yeah, as far as I know

#### Adam Topaz (Nov 23 2020 at 16:22):

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

#### Bhavik Mehta (Nov 23 2020 at 16:30):

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

Last updated: May 19 2021 at 02:10 UTC