How to defined the conjugate of subgroup G be like :

Stream: new members

[Marcus]

263fb3e1-b785-4536-a2d9-9ccfd28e4e6b.png

[Jireh Loreaux]

This is not really a question. Can you provide a #mwe using #backticks ? Also, please be sure to explain what you have tried thus far, and where you are stuck. After doing those things, please ask an explicit question.

[Marcus]

Jireh Loreaux 发言道：

This is not really a question. Can you provide a #mwe using #backticks ? Also, please be sure to explain what you have tried thus far, and where you are stuck. After doing those things, please ask an explicit question.

Thanks for you reply. In fact, I ask this problem's reason is the book mathematics in Lean. In sections of group, chapters 8.1.3 subgroup .The book say use the element of ambient group to defined cojugate. But I think, the ambient group is not really Mathematical terms.I was confused with it.

[Ruben Van de Velde]

If you have a subgroup, it must be sub of something. That something is the ambient group