`BookProof.ChapterAbelianCyclicModel.repState_one` (hxi : ‖xi‖ = 1) : repState pi xi 1 = 1

Initializing...

`BookProof.ChapterAbelianCyclicModel.repState_one` (hxi : ‖xi‖ = 1) : repState pi xi 1 = 1 · Prove2Me