`BookProof.ChapterGravityIrrep.irrep_reconstruction` (M : Matrix (Fin 3) (Fin 3) ℝ) : (1 / 2 : ℝ) • symTracelessPart M + (1 / 2 : ℝ) • antisymPart M + (1 / 3 : ℝ) • (M.trace) • (1

Proved

BookProof.ChapterGravityIrrep.irrep_reconstruction

by leonardopedro · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGravityIrrep.

BookProof.ChapterGravityIrrep.irrep_reconstruction (M : Matrix (Fin 3) (Fin 3) ℝ) : (1 / 2 : ℝ) • symTracelessPart M + (1 / 2 : ℝ) • antisymPart M + (1 / 3 : ℝ) • (M.trace) • (1 : Matrix (Fin 3) (Fin 3) ℝ) = M

Formalization note: Lean 4 identifier BookProof.ChapterGravityIrrep.irrep_reconstruction.

Preamble

-- Generated from ChapterGravityIrrep.lean — theorem BookProof.ChapterGravityIrrep.irrep_reconstruction
import Mathlib
import Definitions.Def_ChapterGravityIrrep
open BookProof.ChapterGravityIrrep



open Matrix
open scoped BigOperators

Formal statement

theorem BookProof.ChapterGravityIrrep.irrep_reconstruction (M : Matrix (Fin 3) (Fin 3) ℝ) :
    (1 / 2 : ℝ) • symTracelessPart M + (1 / 2 : ℝ) • antisymPart M
      + (1 / 3 : ℝ) • (M.trace) • (1 : Matrix (Fin 3) (Fin 3) ℝ) = M := by sorry

View graph