Theorems · Theorem · nonassociative algebras

LieSubalgebra.comap_lieSpan_range_eq

∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L)
  {ι : Type u_1} (f : ι → ↥K),
  LieSubalgebra.comap K.incl (LieSubalgebra.lieSpan R L (Set.range (Subtype.val ∘ f))) =
    LieSubalgebra.lieSpan R (↥K) (Set.range f)

Defined in

Mathlib.Algebra.Lie.Subalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebra