def Hex.PermGroup.Partition.blockSize {n : Nat} (p : Partition n) (x : Fin n) : Nat

Number of points in the block through a point, including that point.

Equations

• p.blockSize x = List.countP (fun (y : Fin n) => decide (p.Same x y)) (List.finRange n)

theorem Hex.PermGroup.Partition.blockSize_pos {n : Nat} (p : Partition n) (x : Fin n) : 0 < p.blockSize x

theorem Hex.PermGroup.Partition.blockSize_image {n : Nat} (p : Partition n) {G : Group n} (hp : p.IsInvariant G) {g : Perm n} (hg : Generated G.generators g) (x : Fin n) : p.blockSize x = p.blockSize (g.get x)

Group elements biject the points in a block with the points in its image.

theorem Hex.PermGroup.Partition.blockSize_eq {n : Nat} (p : Partition n) {G : Group n} (hp : p.IsInvariant G) (ht : G.isTransitive = true) (x y : Fin n) : p.blockSize x = p.blockSize y

Equal block sizes require transitivity; invariant partitions of an intransitive action can have unequal block sizes.