Theorem RootPairing.GeckConstruction.h_def

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_def View on Github →