Theorems · Theorem · nonassociative algebras

LieHom.prod_ext

∀ (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.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₂) → f = g

Split equality of Lie algebra homomorphisms from a product into Lie algebra homomorphism over each component, to allow ext to apply lemmas specific to L₁ →ₗ L and L₂ →ₗ L. See note [partially-applied ext lemmas].

Defined in

Mathlib.Algebra.Lie.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebraLieRingLieAlgebra