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⁻¹

@[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

def Hex.PermGroup.permOfImages (n : ℕ) (l : List ℕ) : Equiv.Perm (Fin n)

A Mathlib permutation from literal images, with the Hex identity fallback.

Equations

• Hex.PermGroup.permOfImages n l = (Hex.Perm.ofImages n l).toEquiv