@[instance_reducible]

instance Hex.instGroupPerm_hexPermGroupMathlib {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.toEquiv {n : ℕ} (p : Perm n) : Fin n ≃ Fin n

The equivalence of Fin n given by a forward permutation: p.get one way, p.inv.get the other.

Equations

• p.toEquiv = { toFun := p.get, invFun := p.inv.get, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Hex.Perm.toEquiv_apply {n : ℕ} (p : Perm n) (i : Fin n) : p.toEquiv i = p.get i

def Hex.Perm.ofEquiv {n : ℕ} (e : Fin n ≃ Fin n) : Perm n

The forward permutation with the same action as an equivalence of Fin n.

Equations

• Hex.Perm.ofEquiv e = Hex.Perm.ofFn ⇑e ⋯ ⋯

@[simp]

theorem Hex.Perm.get_ofEquiv {n : ℕ} (e : Fin n ≃ Fin n) (i : Fin n) : (ofEquiv e).get i = e i

@[simp]

theorem Hex.Perm.ofEquiv_toEquiv {n : ℕ} (p : Perm n) : ofEquiv p.toEquiv = p

@[simp]

theorem Hex.Perm.toEquiv_ofEquiv {n : ℕ} (e : Equiv.Perm (Fin n)) : (ofEquiv e).toEquiv = e

@[simp]

theorem Hex.Perm.toEquiv_id {n : ℕ} : (Perm.id n).toEquiv = 1

@[simp]

theorem Hex.Perm.toEquiv_comp {n : ℕ} (p q : Perm n) : (p.comp q).toEquiv = p.toEquiv * q.toEquiv

@[simp]

theorem Hex.Perm.toEquiv_inv {n : ℕ} (p : Perm n) : p.inv.toEquiv = p.toEquiv⁻¹

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.ofEquiv_one {n : ℕ} : ofEquiv 1 = Perm.id n

@[simp]

theorem Hex.Perm.ofEquiv_mul {n : ℕ} (p q : Equiv.Perm (Fin n)) : ofEquiv (p * q) = (ofEquiv p).comp (ofEquiv q)

@[simp]

theorem Hex.Perm.ofEquiv_inv {n : ℕ} (p : Equiv.Perm (Fin n)) : ofEquiv p⁻¹ = (ofEquiv p).inv

@[simp]

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