Theorems · Theorem · nonassociative algebras

LieAlgebra.IsKilling.biSup_corootSpace_eq_top

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L], ⨆ α, ⨆ (_ : α.IsNonZero), LieAlgebra.corootSpace ⇑α = ⊤

Defined in: Mathlib.Algebra.Lie.Weights.RootSystem
Cited by: 2 results in Mathlib
Foundations: Depth 208 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.

Cites33

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
Setproof · cited by 53,352
Moduleproof · cited by 20,661
Semiringproof · cited by 13,802
AddCommMonoidproof · cited by 12,281
Top.topstatement and proof · cited by 9,680
Fieldstatement and proof · cited by 7,404
Set.rangeproof · cited by 4,705
Set.iUnionproof · cited by 2,483
iSupstatement and proof · cited by 2,415
Set.extproof · cited by 2,266
FiniteDimensionalstatement and proof · cited by 1,854

Cited by2

Results whose statement or proof uses this declaration.

LieIdeal.restr_inf_cartan_eq_biSup_corootSubmoduleproof · cited by 1
LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartanproof · cited by 0