Theorems · Theorem · nonassociative algebras

LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L)
  {α : ↥LieSubalgebra.root},
  α ∈ I.rootSet → ∀ {β : ↥LieSubalgebra.root}, β ∉ I.rootSet → ↑α (LieAlgebra.IsKilling.coroot ↑β) = 0

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites27

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

DFunLike.coestatement · cited by 62,936
Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
Fieldstatement and proof · cited by 7,404
Submoduleproof · cited by 7,192
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
LieSubalgebrastatement and proof · cited by 418
LieIdealstatement and proof · cited by 282
LieModule.Weightstatement and proof · cited by 172

Cited by2

Results whose statement or proof uses this declaration.

LieIdeal.mem_rootSet_of_mem_rootSpanproof · cited by 1
LieIdeal.restr_inf_cartan_eq_biSup_corootSubmoduleproof · cited by 1