issue with groups

Stream: new members

[Andrea Bourque]

hi. I have defined groups A,B,C such that C is a subgroup of B and B is a subgroup of A, as follows:

{A : Type*} [Group A] {B : Subgroup A} {C : Subgroup B}

Furthermore, I use [C.Normal] to assume C is normal in B. However, I get the following error when trying to form the quotient B/C:

failed to synthesize instance
HDiv (Subgroup A) (Subgroup ↥B) ?m.519802

How to I fix this?

[Adam Topaz]

I think you’re using the wrong /

[Adam Topaz]

Write it using \/

[Adam Topaz]

Just / is division as in division of numbers

[Andrea Bourque]

That fixes it, thanks!

[Andrea Bourque]

Another question: How can I make lean treat C as a subgroup of A?

[Andrea Bourque]

I can do it with the inclusion map B -> A, but I can't figure out how to construct it. The docs use a different setup

[Patrick Massot]

Subgroup.map (Subgroup.subtype B) C

[Patrick Massot]

See docs#Subgroup.subtype and docs#Subgroup.map

[Andrea Bourque]

Thanks!

[Andrea Bourque]

Okay, one more question. I'm trying to define the subgroup of A given by aCa^-1 for some a in A. I did the above thing to make C a subgroup of A. I looked in past messages here and saw that this is doable but I didn't understand how to do it

edit: Solved thanks to Yaël