Theorems · Theorem · nonassociative algebras

LieHom.fst_prod

∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂), (LieHom.fst R L₁ L₂).comp (f.prod g) = f

Defined in

Mathlib.Algebra.Lie.Prod

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebraLieRingLieAlgebra