`BookProof.QuantumGravityBrstCharge.linGen_sub` (A B : Matrix (Fin d) (Fin d) ℝ) : linGen (A - B) = linGen A

Initializing...

`BookProof.QuantumGravityBrstCharge.linGen_sub` (A B : Matrix (Fin d) (Fin d) ℝ) : linGen (A - B) = linGen A - linGen B · Prove2Me