Theorems · Theorem · nonassociative algebras

LieAlgebra.IsExtension.range_eq_top

∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L}
  {inst_2 : LieAlgebra R L} {inst_3 : LieRing N} {inst_4 : LieAlgebra R N} {inst_5 : LieRing M}
  {inst_6 : LieAlgebra R M} (i : N →ₗ⁅R⁆ L) {p : L →ₗ⁅R⁆ M} [self : LieAlgebra.IsExtension i p], p.range = ⊤

Defined in

Mathlib.Algebra.Lie.Extension

Cited by

1 results in Mathlib

Foundations

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

Assumes

LieAlgebra.IsExtension