`BookProof.QuantumGravityBrstCharge.linGen_smul_sum` {n : ℕ} (c : Fin n → ℝ) (M : Fin n → Matrix (Fin d) (Fin d) ℝ) : linGen (∑ e, c e • M e) = ∑ e, c e • linGen (M e)

Initializing...

`BookProof.QuantumGravityBrstCharge.linGen_smul_sum` {n : ℕ} (c : Fin n → ℝ) (M : Fin n → Matrix (Fin d) (Fin d) ℝ) : linGen (∑ e, c e • M e) = ∑ e, c e • linGen (M e) · Prove2Me