`BookProof.QuantizationWeyl.comm_scaled` (a b : ℝ) : (a • Xgen) * (b • Ygen) - (b • Ygen) * (a • Xgen) = (a * b) • Zgen

Initializing...

`BookProof.QuantizationWeyl.comm_scaled` (a b : ℝ) : (a • Xgen) * (b • Ygen) - (b • Ygen) * (a • Xgen) = (a * b) • Zgen · Prove2Me