Theorems · Theorem · nonassociative algebras

LieHom.mk_coe

∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y)
  (h₂ :
    ∀ (m : R) (x : L₁),
      { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x)
  (h₃ :
    ∀ {x y : L₁},
      { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
        ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
          { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆),
  { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebra