`BookProof.PermSector.signRep_mem_sectorDom` (n : ℕ) (σ : Equiv.Perm (Fin n)) (x : (Hs.pow n).carrier) (hx : x ∈ sectorDom Hs D₂ n) : (signRep Hs n).act σ x ∈ sectorDom Hs D₂ n

Initializing...

`BookProof.PermSector.signRep_mem_sectorDom` (n : ℕ) (σ : Equiv.Perm (Fin n)) (x : (Hs.pow n).carrier) (hx : x ∈ sectorDom Hs D₂ n) : (signRep Hs n).act σ x ∈ sectorDom Hs D₂ n · Prove2Me