Structures · Algebra
LieRinehartRing
A Lie-Rinehart ring is a pair consisting of a commutative ring A and a Lie ring L such that
A and L are each a module over the other, satisfying compatibility conditions.
- Defined in
- Mathlib.Algebra.LieRinehartAlgebra.Defs
- Shape
- 2 explicit arguments · adds lie_smul_eq_mul', leibniz_mul_right', leibniz_smul_right'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- LieRinehartSubalgebra.toLieSubalgebra
- LieRinehartAlgebra.anchor
- LieRinehartRing.lie_smul_eq_mul'
- LieRinehartRing.leibniz_mul_right'
- LieRinehartSubalgebra.toLieSubalgebra_injective
- LieRinehartSubalgebra.incl
- LieRinehartRing.leibniz_smul_right'
- LieRinehartRing.lie_smul_eq_mul
- LieRinehartAlgebra.anchor_apply
- LieRinehartSubalgebra.coe_incl
- LieRinehartSubalgebra.coe_toLieSubalgebra
- LieRinehartSubalgebra.lieAlgebra
- LieRinehartSubalgebra.instLieRinehartAlgebraSubtypeMem
- LieRinehartRing.leibniz_mul_right
- LieRinehartRing.leibniz_smul_right
- LieRinehartSubalgebra.toLieSubalgebra_inj
- LieRinehartAlgebra.congr_simp
- LieRinehartSubalgebra.lieModule
- LieRinehartSubalgebra.instLieRinehartRingSubtypeMem
Ancestors0
No ancestors.