Theorems · Theorem · nonassociative algebras

LieHom.range_inl

∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂],
  (LieHom.inl R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (LieHom.snd R L₁ L₂).ker

Defined in

Mathlib.Algebra.Lie.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebra