`BookProof.QuantizationWeyl.sum_YZ` (a b : ℝ) : b • Ygen + (a * b) • Zgen = Ngen 0 b (a * b)

Initializing...

`BookProof.QuantizationWeyl.sum_YZ` (a b : ℝ) : b • Ygen + (a * b) • Zgen = Ngen 0 b (a * b) · Prove2Me