Zulip Chat Archive

Stream: Is there code for X?

Topic: has_mem for subgroup of units


view this post on Zulip Adam Topaz (Nov 23 2020 at 15:39):

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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 23 2020 at 16:07):

Works for me! Dirty mathlib?

view this post on Zulip 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

view this post on Zulip 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?!

view this post on Zulip Bhavik Mehta (Nov 23 2020 at 16:21):

Yeah, as far as I know

view this post on Zulip 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?

view this post on Zulip 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