`BookProof.ChapterGravityIrrep.antisymPart_antisymm` (M : Matrix (Fin 3) (Fin 3) ℝ) : (antisymPart M)ᵀ = -(antisymPart M)

Initializing...

`BookProof.ChapterGravityIrrep.antisymPart_antisymm` (M : Matrix (Fin 3) (Fin 3) ℝ) : (antisymPart M)ᵀ = -(antisymPart M) · Prove2Me