mathlib3 documentation


Extension and restriction of scalars for Lie algebras #

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

Lie algebras have a well-behaved theory of extension and restriction of scalars.

Main definitions #

Tags #

lie ring, lie algebra, extension of scalars, restriction of scalars, base change

@[protected, instance]
theorem lie_algebra.extend_scalars.bracket_tmul (R : Type u) (A : Type w) (L : Type v) [comm_ring R] [comm_ring A] [algebra R A] [lie_ring L] [lie_algebra R L] (s t : A) (x y : L) :