Theorems · Theorem · nonassociative algebras

LieAlgebra.IsKilling.rootSystem_root_apply

∀ {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] (α : ↥LieSubalgebra.root),
  (LieAlgebra.IsKilling.rootSystem H).root α = LieModule.Weight.toLinear K (↥H) L ↑α

Defined in: Mathlib.Algebra.Lie.Weights.RootSystem
Cited by: 1 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.

Cites19

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

DFunLike.coestatement · cited by 62,936
RingHom.idstatement · cited by 18,349
Finsetstatement · cited by 13,712
Fieldstatement and proof · cited by 7,404
FiniteDimensionalstatement and proof · cited by 1,854
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
Function.Embeddingstatement · cited by 988
CharZerostatement and proof · cited by 932
Module.Dualstatement · cited by 583
LieSubalgebrastatement and proof · cited by 418
RootPairing.rootstatement · cited by 326

Cited by1

Results whose statement or proof uses this declaration.

LieAlgebra.IsKilling.lieIdealOrderIso_left_invproof · cited by 0