structure Hex.PermGroup.Bijection (α β : Type) : Type

Mutually inverse maps, without a dependency on Mathlib's Equiv.

• toFun : α → β

  The forward map.

• invFun : β → α

  The inverse map.

• left_inv (x : α) : self.invFun (self.toFun x) = x

  Inverting the forward map recovers its input.

• right_inv (y : β) : self.toFun (self.invFun y) = y

  Applying the forward map after its inverse recovers its input.

def Hex.PermGroup.Bijection.refl (α : Type) : Bijection α α

Equations

• Hex.PermGroup.Bijection.refl α = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ }

def Hex.PermGroup.Bijection.trans {α β γ : Type} (f : Bijection α β) (g : Bijection β γ) : Bijection α γ

Equations

• f.trans g = { toFun := fun (x : α) => g.toFun (f.toFun x), invFun := fun (z : γ) => f.invFun (g.invFun z), left_inv := ⋯, right_inv := ⋯ }

def Hex.PermGroup.Bijection.prod {α β γ δ : Type} (f : Bijection α β) (g : Bijection γ δ) : Bijection (α × γ) (β × δ)

Equations

• f.prod g = { toFun := fun (x : α × γ) => (f.toFun x.fst, g.toFun x.snd), invFun := fun (y : β × δ) => (f.invFun y.fst, g.invFun y.snd), left_inv := ⋯, right_inv := ⋯ }

def Hex.PermGroup.Bijection.finMul (a b : Nat) : Bijection (Fin a × Fin b) (Fin (a * b))

Mixed-radix encoding of a pair of finite indices.

Equations

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

def Hex.PermGroup.HasOrder {n : Nat} (S : Array (Perm n)) (N : Nat) : Prop

The subgroup generated by S has exactly N elements: its elements admit mutually inverse ranking and unranking maps to Fin N.

Equations

• Hex.PermGroup.HasOrder S N = Nonempty (Hex.PermGroup.Bijection { p : Hex.Perm n // Hex.PermGroup.Generated S p } (Fin N))