Zulip Chat Archive

Stream: Is there code for X?

Topic: Mᵐᵒᵖˣ vs Mˣᵐᵒᵖ

Johan Commelin (Jan 06 2024 at 18:15):

Do we have the group isomorphism between Mᵐᵒᵖˣ and Mˣᵐᵒᵖ?

Yaël Dillies (Jan 06 2024 at 18:22):

Pretty sure we don't

Richard Copley (Jan 06 2024 at 18:25):

Not docs#Units.opEquiv ? (In Mathlib.Algebra.Group.Opposite)

Johan Commelin (Jan 06 2024 at 18:26):

Awesome! Thanks!

Yury G. Kudryashov (Jan 07 2024 at 03:25):

Let me try: @loogle MulEquiv, MulOpposite, Units

loogle (Jan 07 2024 at 03:25):

:search: Units.opEquiv, Units.coe_unop_opEquiv, and 1 more

Yury G. Kudryashov (Jan 07 2024 at 03:25):

Works!

Last updated: May 02 2025 at 03:31 UTC