Theorems · Theorem · nonassociative algebras

LieDerivation.IsKilling.killingForm_restrict_range_ad

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

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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

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.BilinFormstatement and proof · cited by 501
LieSubalgebrastatement and proof · cited by 418
LieDerivationstatement and proof · cited by 95
LieSubalgebra.toSubmodulestatement and proof · cited by 90
LieIdeal.toLieSubalgebraproof · cited by 48
LieHom.rangestatement · cited by 44
killingFormstatement and proof · cited by 34

Cited by2

Results whose statement or proof uses this declaration.

LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerateproof · cited by 1
LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonalproof · cited by 1