noncomputable def Hex.PermGroup.Partition.ofSetoid {n : ℕ} (r : Setoid (Fin n)) : Partition n

Canonical representatives of an arbitrary mathematical equivalence relation. This proof-side construction does not enter the executable block algorithm.

Equations

• Hex.PermGroup.Partition.ofSetoid r = Hex.PermGroup.Partition.ofValues (Hex.Vector.ofFn' fun (x : Fin n) => ⟦x⟧)

theorem Hex.PermGroup.Partition.ofSetoid_same {n : ℕ} (r : Setoid (Fin n)) (x y : Fin n) : (ofSetoid r).Same x y ↔ r x y

theorem Hex.PermGroup.Blocks.class_isBlock {M : Type u_1} {X : Type u_2} [_root_.Group M] [MulAction M X] (r : Setoid X) (hr : ∀ (g : M) (x y : X), r x y ↔ r (g • x) (g • y)) (a : X) : MulAction.IsBlock M {x : X | r a x}

An invariant equivalence class is a block in Mathlib's translate-or-disjoint sense, without assuming that the action is transitive.

def Hex.PermGroup.Blocks.translateSetoid {M : Type u_1} {X : Type u_2} [_root_.Group M] [MulAction M X] (B : Set X) : Setoid X

Indistinguishability by all translates of a subset is an invariant equivalence relation. For a block, all its points are indistinguishable.

Equations

• Hex.PermGroup.Blocks.translateSetoid B = { r := fun (x y : X) => ∀ (g : M), g • x ∈ B ↔ g • y ∈ B, iseqv := ⋯ }

theorem Hex.PermGroup.Blocks.translate_invariant {M : Type u_1} {X : Type u_2} [_root_.Group M] [MulAction M X] (B : Set X) (g : M) (x y : X) : (translateSetoid B) x y ↔ (translateSetoid B) (g • x) (g • y)

theorem Hex.PermGroup.Blocks.related_of_mem {M : Type u_1} {X : Type u_2} [_root_.Group M] [MulAction M X] {B : Set X} (hB : MulAction.IsBlock M B) {x y : X} (hx : x ∈ B) (hy : y ∈ B) : (translateSetoid B) x y

theorem Hex.PermGroup.Partition.blockSystem {n : ℕ} (p : Partition n) {G : Group n} (hp : p.IsInvariant G) : MulAction.IsBlockSystem (↥(closure G.generators)) p.toSetoid.classes

Classes of an invariant partition form a Mathlib block system, also for intransitive actions and unequal class sizes.

theorem Hex.PermGroup.Group.primitive_spec {n : ℕ} (G : Group n) : G.IsPrimitive ↔ 2 ≤ n ∧ MulAction.IsPreprimitive (↥(closure G.generators)) (Fin n)

Mathlib's preprimitivity admits degenerate degrees; the executable primitive convention retains the explicit degree-at-least-two condition.

theorem Hex.PermGroup.Group.isPrimitive_spec {n : ℕ} (G : Group n) : G.isPrimitive = true ↔ 2 ≤ n ∧ MulAction.IsPreprimitive (↥(closure G.generators)) (Fin n)