Theorems · Theorem · nonassociative algebras
SetLike.GradedBracket.bracket_mem
∀ {ι : Type u_1} {σ : Type u_2} {L : Type u_4} {inst : SetLike σ L} {inst_1 : Bracket L L} {inst_2 : Add ι} {ℒ : ι → σ}
[self : SetLike.GradedBracket ℒ] ⦃i j : ι⦄ {gi gj : L}, gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ (i + j)Bracket is homogeneous
- Defined in
- Mathlib.Algebra.Lie.Graded
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- SetLike.GradedBracket
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLikestatement and proof · cited by 1,084
- Bracket.bracketstatement · cited by 642
- Bracketstatement and proof · cited by 8
- SetLike.GradedBracketstatement and proof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.