`BookProof.ChapterCayleyTransform.sub_cayley_shift` (x : T.domain) : T.shift (-1) x - cayley T (T.shift (-1) x) = (2 * Complex.I) • (x : H)

Initializing...

`BookProof.ChapterCayleyTransform.sub_cayley_shift` (x : T.domain) : T.shift (-1) x - cayley T (T.shift (-1) x) = (2 * Complex.I) • (x : H) · Prove2Me