∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : Field K] [inst_3 : CharZero K] [inst_4 : AddCommGroup M] [inst_5 : Module K M] [inst_6 : AddCommGroup N]
  [inst_7 : Module K N] {P : RootPairing ι K M N} [inst_8 : P.IsReduced] [inst_9 : P.IsCrystallographic]
  [inst_10 : P.IsIrreducible] [inst_11 : P.IsRootSystem] (b : P.Base)
  [inst_12 : LieAlgebra.IsKilling K ↥(RootPairing.GeckConstruction.lieAlgebra b)] [inst_13 : IsAlgClosed K],
  (LieAlgebra.IsKilling.rootSystem (RootPairing.GeckConstruction.basis b).cartan).IsReduced