`BookProof.ChapterA3.mgammaR_indep` (c : Fin 4 → ℝ) (h : ∑ ν, c ν • mgammaR ν = 0) : ∀ ν, c ν = 0

Initializing...

`BookProof.ChapterA3.mgammaR_indep` (c : Fin 4 → ℝ) (h : ∑ ν, c ν • mgammaR ν = 0) : ∀ ν, c ν = 0 · Prove2Me