Theorems · Definition · nonassociative algebras

LieAlgebra.IsSolvable.casesOn

{L : Type v} →
  [inst : LieRing L] →
    {motive : LieAlgebra.IsSolvable L → Sort u} →
      (t : LieAlgebra.IsSolvable L) → ((solvable_int : ∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥) → motive ⋯) → motive t

Defined in: Mathlib.Algebra.Lie.Solvable
Cited by: 1 results in Mathlib
Foundations: Depth 43 from the axioms · uses propext, Quot.sound
Assumes: LieRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Bot.botstatement and proof · cited by 4,720
LieRingstatement and proof · cited by 1,548
LieIdealstatement · cited by 282
LieAlgebra.derivedSeriesstatement and proof · cited by 29
LieAlgebra.IsSolvablestatement and proof · cited by 24

Cited by1

Results whose statement or proof uses this declaration.

LieAlgebra.isSolvable_iff_intproof · cited by 0