Zulip Chat Archive

Stream: Is there code for X?

Topic: has_mem for subgroups of units


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

view this post on Zulip Adam Topaz (Aug 27 2020 at 14:06):

Should it even be an instance?

view this post on Zulip Reid Barton (Aug 27 2020 at 14:15):

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

view this post on Zulip Adam Topaz (Aug 27 2020 at 14:19):

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

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

view this post on Zulip Adam Topaz (Aug 27 2020 at 15:36):

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

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

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

view this post on Zulip Adam Topaz (Aug 27 2020 at 19:56):

I agree. What about the out_param thing?

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