Theorem RootPairing.GeckConstruction.h_eq_diagonal

Modification history

2025-08-11 13:25

Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

chore: split file `LinearAlgebra.RootSystem.GeckConstruction.Basic` (#28089) …

Added RootPairing.GeckConstruction.h_eq_diagonal View on Github →