Theorems · Theorem · nonassociative algebras
LieAlgebra.HasTrivialRadical.radical_eq_bot
∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
[self : LieAlgebra.HasTrivialRadical R L], LieAlgebra.radical R L = ⊥- Defined in
- Mathlib.Algebra.Lie.Semisimple.Defs
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LieAlgebra.HasTrivialRadical
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Bot.botstatement · cited by 4,720
- LieRingstatement and proof · cited by 1,548
- LieAlgebrastatement and proof · cited by 1,246
- LieIdealstatement · cited by 282
- LieAlgebra.radicalstatement · cited by 13
- LieAlgebra.HasTrivialRadicalstatement and proof · cited by 11
Cited by2
Results whose statement or proof uses this declaration.
- LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvableproof · cited by 1
- LieAlgebra.abelian_radical_of_hasTrivialRadicalproof · cited by 0