Theorems · Inductive type · nonassociative algebras

SetLike.GradedBracket

{ι : Type u_1} → {σ : Type u_2} → {L : Type u_4} → [SetLike σ L] → [Bracket L L] → [Add ι] → (ι → σ) → Prop

A class that ensures a bracket product preserves an additive grading.

Defined in

Mathlib.Algebra.Lie.Graded

Cited by

1 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SetLikeBracketAdd