Theorems · Inductive type · nonassociative algebras

LieRinehartSubalgebra

(A : Type u_1) → (L : Type u_2) → [inst : CommRing A] → [inst_1 : LieRing L] → [Module A L] → Type u_2

A Lie-Rinehart subalgebra of a Lie-Rinehart algebra (R A L) is an A-submodule of L, which is stable under the Lie bracket. (This can be defined independently of R and most Lie-Rinehart algebra axioms).

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Cited by

29 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingLieRingModule