Theorems · Theorem · nonassociative algebras

LieAlgebra.IsExtension.exact

∀ {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],
  i.range = LieIdeal.toLieSubalgebra R L p.ker

Defined in: Mathlib.Algebra.Lie.Extension
Cited by: 2 results in Mathlib
Foundations: Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LieAlgebra.IsExtension

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
LieSubalgebrastatement · cited by 418
LieHomstatement and proof · cited by 382
LieIdeal.toLieSubalgebrastatement · cited by 48
LieHom.rangestatement · cited by 44
LieHom.kerstatement · cited by 37
LieAlgebra.IsExtensionstatement and proof · cited by 14

Cited by2

Results whose statement or proof uses this declaration.

LieAlgebra.Extension.incl_apply_mem_kerproof · cited by 1
LieAlgebra.Extension.ringModuleOf_bracket_projproof · cited by 1