`BookProof.ChapterA3.isCliffordC_toC` {A : Fin 4 → Matrix (Fin 4) (Fin 4) ℝ} (hA : IsCliffordR A) : IsCliffordC (fun μ => toC (A μ))

Initializing...

`BookProof.ChapterA3.isCliffordC_toC` {A : Fin 4 → Matrix (Fin 4) (Fin 4) ℝ} (hA : IsCliffordR A) : IsCliffordC (fun μ => toC (A μ)) · Prove2Me