Theorems · Theorem · nonassociative algebras

TensorProduct.LieModule.toLinearMap_map

∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃}
  [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N]
  [inst_9 : LieRingModule L N] [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P]
  [inst_13 : LieRingModule L P] [inst_14 : LieModule R L P] [inst_15 : AddCommGroup Q] [inst_16 : Module R Q]
  [inst_17 : LieRingModule L Q] [inst_18 : LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q),
  ↑(TensorProduct.LieModule.map f g) = TensorProduct.map ↑f ↑g

Defined in

Mathlib.Algebra.Lie.TensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModule