Theorems · Theorem · nonassociative algebras
LieAlgebra.toEnd_pow_apply_mem
∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
{H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] {M : Type u_3} [inst_4 : AddCommGroup M]
[inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] {χ₁ χ₂ : ↥H → R} {x : L} {m : M},
x ∈ LieAlgebra.rootSpace H χ₁ →
m ∈ LieModule.genWeightSpace M χ₂ →
∀ (n : ℕ), ((LieModule.toEnd R L M) x ^ n) m ∈ LieModule.genWeightSpace M (n • χ₁ + χ₂)- Defined in
- Mathlib.Algebra.Lie.Weights.Cartan
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
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
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- zero_addproof · cited by 2,366
- LieRingstatement and proof · cited by 1,548
- add_commproof · cited by 1,535
- LieAlgebrastatement and proof · cited by 1,246
- pow_zeroproof · cited by 1,094
- Module.Endstatement · cited by 774
- add_assocproof · cited by 746
Cited by3
Results whose statement or proof uses this declaration.
- LieAlgebra.IsKilling.chainTopCoeff_zero_rightproof · cited by 4
- LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_leproof · cited by 3
- LieModule.isNilpotent_toEnd_of_mem_rootSpaceproof · cited by 1