Theorems · Theorem · nonassociative algebras

LieAlgebra.IsKilling.coroot_mem_corootSpace

∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.coroot α ∈ LieAlgebra.corootSpace ⇑α

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites21

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

DFunLike.coestatement and proof · cited by 62,936
Fieldstatement and proof · cited by 7,404
FiniteDimensionalstatement and proof · cited by 1,854
LieRingstatement and proof · cited by 1,548
LinearEquiv.symmproof · cited by 1,461
LieAlgebrastatement and proof · cited by 1,246
LieSubalgebrastatement and proof · cited by 418
LieIdealstatement · cited by 282
LieRing.ofAssociativeRingstatement · cited by 227
Submodule.smul_memproof · cited by 204
LieModule.Weightstatement and proof · cited by 172
LieSubmodule.toSubmoduleproof · cited by 150

Cited by1

Results whose statement or proof uses this declaration.

LieAlgebra.IsKilling.coe_coroot_mem_corootSubmoduleproof · cited by 2