def Hex.Perm.Wreath.index {n m : Nat} (i : Fin n) (j : Fin m) : Fin (n * m)

The point i of block j has label j*n+i.

Equations

• Hex.Perm.Wreath.index i j = ⟨↑j * n + ↑i, ⋯⟩

theorem Hex.Perm.Wreath.pos_of_lt_mul {n m : Nat} (x : Fin (n * m)) : 0 < n

A point of the product degree witnesses that blocks are nonempty.

def Hex.Perm.Wreath.point {n m : Nat} (x : Fin (n * m)) : Fin n

Equations

• Hex.Perm.Wreath.point x = ⟨↑x % n, ⋯⟩

def Hex.Perm.Wreath.block {n m : Nat} (x : Fin (n * m)) : Fin m

Equations

• Hex.Perm.Wreath.block x = ⟨↑x / n, ⋯⟩

@[simp]

theorem Hex.Perm.Wreath.point_index {n m : Nat} (i : Fin n) (j : Fin m) : point (index i j) = i

@[simp]

theorem Hex.Perm.Wreath.block_index {n m : Nat} (i : Fin n) (j : Fin m) : block (index i j) = j

@[simp]

theorem Hex.Perm.Wreath.index_point_block {n m : Nat} (x : Fin (n * m)) : index (point x) (block x) = x

theorem Hex.Perm.Wreath.index_injective {n m : Nat} {i a : Fin n} {j b : Fin m} (h : index i j = index a b) : i = a ∧ j = b