Structures · Algebra
LieDerivation.SMulBracketCommClass
A typeclass mixin saying that scalar multiplication and Lie bracket are left commutative.
- Defined in
- Mathlib.Algebra.Lie.Derivation.Basic
- Shape
- 3 explicit arguments · adds smul_bracket_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by9
Ancestors0
No ancestors.