@[instance_reducible]

instance Hex.instGroupPerm_hexPermGroupTheory {n : ℕ} : Group (Perm n)

Mathlib's group structure uses the computational permutation operations, including the same left-recursive natural power implementation.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Perm.equiv {n : ℕ} : Perm n ≃* Equiv.Perm (Fin n)

Executable permutations and Mathlib permutations, with the same multiplication order and left action on the declared domain.

Equations

• Hex.Perm.equiv = { toFun := Hex.Perm.toEquiv, invFun := Hex.Perm.ofEquiv, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem Hex.Perm.toEquiv_pow {n : ℕ} (p : Perm n) (k : ℕ) : (p.pow k).toEquiv = p.toEquiv ^ k