Theorems · Theorem · nonassociative algebras

LieHom.prod_ext_iff

∀ (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 g : L₁ × L₂ →ₗ⁅R⁆ L},
  f = g ↔
    f.comp (LieHom.inl R L₁ L₂) = g.comp (LieHom.inl R L₁ L₂) ∧
      f.comp (LieHom.inr R L₁ L₂) = g.comp (LieHom.inr R L₁ L₂)

Defined in

Mathlib.Algebra.Lie.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebraLieRingLieAlgebra