Theorems · Theorem · nonassociative algebras

LieRinehartAlgebra.Hom.map_smul_apply

∀ {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [inst : CommRing R]
  [inst_1 : CommRing A₁] [inst_2 : LieRing L₁] [inst_3 : Module A₁ L₁] [inst_4 : LieRingModule L₁ A₁]
  [inst_5 : CommRing A₂] [inst_6 : LieRing L₂] [inst_7 : Module A₂ L₂] [inst_8 : LieRingModule L₂ A₂]
  [inst_9 : Algebra R A₁] [inst_10 : LieAlgebra R L₁] [inst_11 : Algebra R A₂] [inst_12 : LieAlgebra R L₂]
  {σ₁₂ : A₁ →ₐ[R] A₂} (f : LieRinehartAlgebra.Hom σ₁₂ L₁ L₂) (a : A₁) (x : L₁),
  f.toLieHom (a • x) = σ₁₂ a • f.toLieHom x

This is LieRinehartAlgebra.Hom.map_smul_apply' restated using the coercion to function rather than LieRinehartAlgebra.Hom.toLieHom.

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext

Assumes

CommRingCommRingLieRingModuleLieRingModuleCommRingLieRingModuleLieRingModuleAlgebraLieAlgebraAlgebraLieAlgebra