Theorems · Theorem · nonassociative algebras

LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  (LieAlgebra.IsKilling.rootSystem H).CorootForm = (killingForm K L).restrict H.toSubmodule

Defined in: Mathlib.Algebra.Lie.Weights.RootSystem
Cited by: 0 results in Mathlib
Foundations: Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field CharZero LieRing LieAlgebra LieAlgebra.IsKilling FiniteDimensional LieSubalgebra.IsCartanSubalgebra LieModule.IsTriangularizable

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites28

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHom.idstatement and proof · cited by 18,349
Finsetstatement · cited by 13,712
LinearMapproof · cited by 10,215
Fieldstatement and proof · cited by 7,404
Finset.sumproof · cited by 5,195
FiniteDimensionalstatement and proof · cited by 1,854
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
CharZerostatement and proof · cited by 932
Module.Dualstatement · cited by 583
LinearMap.BilinFormstatement and proof · cited by 501
LieSubalgebrastatement and proof · cited by 418

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.