mathlib3 documentation

ring_theory.derivation.lie

Results #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Lie structures #

@[protected, instance]
def derivation.has_bracket {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] :

The commutator of derivations is again a derivation.

Equations
@[simp]
theorem derivation.commutator_coe_linear_map {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {D1 D2 : derivation R A A} :
theorem derivation.commutator_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {D1 D2 : derivation R A A} (a : A) :
D1, D2 a = D1 (D2 a) - D2 (D1 a)