Theorems · Definition · nonassociative algebras

LieSubalgebra.topEquiv

{R : Type u} → {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → ↥⊤ ≃ₗ⁅R⁆ L

The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra. This is the Lie subalgebra version of Submodule.topEquiv.

Defined in

Mathlib.Algebra.Lie.Submodule

Cited by

3 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebra