Commit 2025-08-11 13:25 337e0bcf

chore: split file LinearAlgebra.RootSystem.GeckConstruction.Basic (#28089) The contents of Relations.lean are just a simple copy-paste, likewise almost all of Semisimple.lean The changes which are not pure deletion / copy-paste arise since we wish to keep the lemma cartanSubalgebra_le_lieAlgebra out of Relations.lean and to have the lemma trace_toEnd_eq_zero not depend on Relations.lean. We thus need to remove dependence on lie_e_f_same, and to do this we must adjust the definitions of RootPairing.GeckConstruction.lieAlgebra and RootPairing.GeckConstruction.cartanSubalgebra.