Documentation Verification Report

Killing

📁 Source: Mathlib/Algebra/Lie/Killing.lean

Statistics

Metric	Count
Definitions `IsKilling`	1
Theorems `ideal_eq_bot_of_isLieAbelian`, `instHasTrivialRadical`, `instSemisimple`, `ker_killingForm_eq_bot`, `killingCompl_top_eq_bot`, `killingForm_nondegenerate`, `isKilling_of_equiv`, `killingForm_of_equiv_apply`, `isKilling`, `isCompl_killingCompl`	10
Total	11

LieAlgebra

Definitions

Name	Category	Theorems
`IsKilling` 📖	CompData	3 math math: `LieDerivation.IsKilling.instIsKilling_range_ad`, `isKilling_of_equiv`, `LieEquiv.isKilling`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isKilling_of_equiv` 📖	mathematical	—	`IsKilling`	—	`LieSubmodule.ext` `lieAlgebraSelfModule` `LieModule.traceForm_comm` `LinearMap.ext` `killingForm_of_equiv_apply` `LieEquiv.apply_symm_apply` `RingHomInvPair.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearEquiv.congr_arg` `IsKilling.ker_killingForm_eq_bot` `LinearMap.map_zero₂`
`killingForm_of_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `LieEquiv` `EquivLike.toFunLike` `LieEquiv.instEquivLike`	—	`smulCommClass_self` `RingHomCompTriple.ids` `IsScalarTower.left` `killingForm_apply_apply` `RingHomInvPair.ids` `LinearMap.comp.congr_simp` `LinearMap.trace_conj'`

LieAlgebra.IsKilling

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ideal_eq_bot_of_isLieAbelian` 📖	mathematical	—	`Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `eq_bot_iff` `killingCompl_top_eq_bot` `LieIdeal.le_killingCompl_top_of_isLieAbelian`
`instHasTrivialRadical` 📖	mathematical	—	`LieAlgebra.HasTrivialRadical`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals` `ideal_eq_bot_of_isLieAbelian`
`instSemisimple` 📖	mathematical	—	`LieAlgebra.IsSemisimple` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`LieAlgebra.InvariantForm.isSemisimple_of_nondegenerate` `killingForm_nondegenerate` `LieModule.traceForm_lieInvariant` `lieAlgebraSelfModule` `LinearMap.IsSymm.isRefl` `LieModule.traceForm_isSymm` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `ideal_eq_bot_of_isLieAbelian` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`ker_killingForm_eq_bot` 📖	mathematical	—	`LinearMap.ker` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `Bot.bot` `Submodule` `Submodule.instBot`	—	`killingCompl_top_eq_bot`
`killingCompl_top_eq_bot` 📖	mathematical	—	`LieIdeal.killingCompl` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `Bot.bot` `LieSubmodule.instBot`	—	—
`killingForm_nondegenerate` 📖	mathematical	—	`LinearMap.BilinForm.Nondegenerate` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `killingForm`	—	`lieAlgebraSelfModule` `LinearMap.IsRefl.nondegenerate_iff_separatingLeft` `LinearMap.IsSymm.isRefl` `LieModule.traceForm_isSymm` `smulCommClass_self` `ker_killingForm_eq_bot`

LieEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isKilling` 📖	mathematical	—	`LieAlgebra.IsKilling`	—	`LieAlgebra.isKilling_of_equiv`

LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompl_killingCompl` 📖	mathematical	—	`IsCompl` `LieIdeal` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice` `killingCompl`	—	`LieAlgebra.IsKilling.instSemisimple` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `lieAlgebraSelfModule` `LieModule.traceForm_apply_lie_apply` `LieModule.traceForm_comm` `mem_killingCompl` `lie_mem_left` `LieSubmodule.lie_abelian_iff_lie_self_eq_bot` `LieSubmodule.lie_eq_bot_iff` `LieAlgebra.IsKilling.killingForm_nondegenerate` `disjoint_iff` `LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieSubmodule.isCompl_toSubmodule` `toSubmodule_killingCompl` `LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint` `LinearMap.IsSymm.isRefl` `LieModule.traceForm_isSymm` `LieSubmodule.disjoint_toSubmodule`

---

← Back to Index