Group isomorphisms Lean 4

Stream: Is there code for X?

[Isabel Dahlgren]

Hi all,
I'm trying to define an isomorphism between two multiplicative groups G and H. I found the mul_equiv in Lean 3, but I can't find an analogue in Lean 4. Any help would be much appreciated.

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (φ : G ≃ H) -- ≃* doesn't work

#check mul_assoc
#check φ.toFun -- φ.toFun : G → H
#check φ.4 -- φ.right_inv : Function.RightInverse φ.invFun φ.toFun

[Riccardo Brasca]

It's called docs#MulEquiv

[Riccardo Brasca]

And the notation is ≃*.

[Riccardo Brasca]

If this doesn't work for you you probably need to import Mathlib.Algebra.Hom.Equiv.Basic.

[Isabel Dahlgren]

Riccardo Brasca said:

It's called docs#MulEquiv

Oh, that works. Thanks! :ok:

[Yury G. Kudryashov]

There is a #lookup3 command.

[Yury G. Kudryashov]

Or you can git grep '#align mul_equiv'

[Calvin Lee]

Yury G. Kudryashov said:

There is a #lookup3 command.

wow, i sure wasted a lot of time porting files by ripgreping through mathlib4 for aligns