Theorems · Theorem · nonassociative algebras

LieRinehartAlgebra.anchor_apply

∀ {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : LieRing L₁]
  [inst_3 : Module A₁ L₁] [inst_4 : LieRingModule L₁ A₁] [inst_5 : Algebra R A₁] [inst_6 : LieAlgebra R L₁]
  [inst_7 : LieRinehartRing A₁ L₁] [inst_8 : LieRinehartAlgebra R A₁ L₁] (l : L₁) (a : A₁),
  ((LieRinehartAlgebra.anchor R A₁ L₁).toLieHom l) a = ⁅l, a⁆

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingLieRingModuleLieRingModuleAlgebraLieAlgebraLieRinehartRingLieRinehartAlgebra