`BookProof.ChapterCayleyTransform.range_one_sub_cayley` : Set.range (fun y : H => y - cayley T y) = (T.domain : Set H)

Initializing...

`BookProof.ChapterCayleyTransform.range_one_sub_cayley` : Set.range (fun y : H => y - cayley T y) = (T.domain : Set H) · Prove2Me