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

Initializing...

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