Theorem RootPairing.GeckConstruction.ω_mul_ω
Modification history
2025-08-11 08:45
Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean
feat: the Geck Construction yields trace-free matrices (#27831) …
Modified RootPairing.GeckConstruction.ω_mul_ωView on Github →