`BookProof.ChapterA4f.boostZ_mul_inv` {l : ℂ} (hl : l ≠ 0) : boostZ l * boostZ l⁻¹ = 1

Initializing...

`BookProof.ChapterA4f.boostZ_mul_inv` {l : ℂ} (hl : l ≠ 0) : boostZ l * boostZ l⁻¹ = 1 · Prove2Me