Theorems · Theorem · nonassociative algebras

LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate

∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  [LieAlgebra.IsKilling R L],
  ((killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule).Nondegenerate

The restriction of the Killing form of a finite-dimensional Killing Lie algebra to the range of the adjoint action is nondegenerate.

Defined in: Mathlib.Algebra.Lie.Derivation.Killing
Cited by: 1 results in Mathlib
Foundations: Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LieRing LieAlgebra Module.Finite LieAlgebra.IsKilling

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites19

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

Moduleproof · cited by 20,661
AddCommMonoidproof · cited by 12,281
CommSemiringproof · cited by 10,911
Fieldstatement and proof · cited by 7,404
Submodulestatement · cited by 7,192
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
Module.Finitestatement and proof · cited by 1,032
LinearMap.BilinFormproof · cited by 501
LieAlgebra.IsKillingstatement and proof · cited by 122
LieDerivationstatement and proof · cited by 95
LieSubalgebra.toSubmodulestatement and proof · cited by 90

Cited by1

Results whose statement or proof uses this declaration.

LieDerivation.IsKilling.range_ad_eq_topproof · cited by 1