`BookProof.ChapterGravityPolymomentum.contract_smul_left` (c : ℝ) (A B : Matrix (Fin 4) (Fin 4) ℝ) : contract (c • A) B = c * contract A B

Initializing...

`BookProof.ChapterGravityPolymomentum.contract_smul_left` (c : ℝ) (A B : Matrix (Fin 4) (Fin 4) ℝ) : contract (c • A) B = c * contract A B · Prove2Me