Theorems · Definition · nonassociative algebras

LieModule.IsTrivial.casesOn

{L : Type v} →
  {M : Type w} →
    [inst : Bracket L M] →
      [inst_1 : Zero M] →
        {motive : LieModule.IsTrivial L M → Sort u} →
          (t : LieModule.IsTrivial L M) → ((trivial : ∀ (x : L) (m : M), ⁅x, m⁆ = 0) → motive ⋯) → motive t

Defined in: Mathlib.Algebra.Lie.Abelian
Cited by: 2 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms
Assumes: Bracket Zero

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

Bracket.bracketstatement and proof · cited by 642
LieModule.IsTrivialstatement and proof · cited by 14
Bracketstatement and proof · cited by 8

Cited by2

Results whose statement or proof uses this declaration.

LieModule.isTrivial_iff_max_triv_eq_topproof · cited by 1
LieModule.trivial_iff_le_maximal_trivialproof · cited by 0