Killing

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

Statistics

Metric	Count
Definitions rangeAdOrthogonal	1
Theorems ad_apply_eq_zero_iff, ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, ad_mem_orthogonal_of_mem_orthogonal, exists_eq_ad, instIsKilling_range_ad, killingForm_restrict_range_ad, killingForm_restrict_range_ad_nondegenerate, rangeAdOrthogonal_carrier, range_ad_eq_top	9
Total	10

LieDerivation.IsKilling

Definitions

Name	Category	Theorems
rangeAdOrthogonal 📖	CompOp	1 math math: rangeAdOrthogonal_carrier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ad_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe LieHom LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule LieDerivation.instLieRing LieDerivation.instLieAlgebra LieHom.instFunLike LieDerivation.ad LieDerivation.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	lieAlgebraSelfModule LieSubmodule.mem_bot LieAlgebra.center_eq_bot LieAlgebra.instIsFaithfulOfHasTrivialRadical LieAlgebra.IsKilling.instHasTrivialRadical Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LieDerivation.ad_ker_eq_center LieHom.mem_ker map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass
ad_mem_ker_killingForm_ad_range_of_mem_orthogonal 📖	mathematical	LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieDerivation.instLieRing LieDerivation.instLieAlgebra SetLike.instMembership Submodule.setLike LinearMap.BilinForm.orthogonal killingForm LieSubalgebra.toSubmodule LieHom.range LieDerivation.ad	Submodule.map Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.subtype LinearMap.ker LieSubalgebra LieSubalgebra.instSetLike LinearMap LieSubalgebra.lieRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieSubalgebra.lieAlgebra Semiring.toModule LinearMap.addCommMonoid LinearMap.module DFunLike.coe LieHom LieHom.instFunLike LieDerivation.instFunLike	—	lieAlgebraSelfModule RingHomSurjective.ids killingForm_restrict_range_ad LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict smulCommClass_self LieDerivation.instSMulBase LinearMap.IsSymm.isRefl LieModule.traceForm_isSymm ad_mem_orthogonal_of_mem_orthogonal
ad_mem_orthogonal_of_mem_orthogonal 📖	mathematical	LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieDerivation.instLieRing LieDerivation.instLieAlgebra SetLike.instMembership Submodule.setLike LinearMap.BilinForm.orthogonal killingForm LieSubalgebra.toSubmodule LieHom.range LieDerivation.ad	DFunLike.coe LieHom LieHom.instFunLike LieDerivation.instFunLike	—	lieAlgebraSelfModule RingHomSurjective.ids AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass LieSubmodule.lie_mem smulCommClass_self LieDerivation.instSMulBase
exists_eq_ad 📖	mathematical	—	DFunLike.coe LieHom LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule LieDerivation.instLieRing LieDerivation.instLieAlgebra LieHom.instFunLike LieDerivation.ad	—	lieAlgebraSelfModule range_ad_eq_top Submodule.mem_top
instIsKilling_range_ad 📖	mathematical	—	LieAlgebra.IsKilling LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule LieSubalgebra LieDerivation.instLieRing LieDerivation.instLieAlgebra SetLike.instMembership LieSubalgebra.instSetLike LieHom.range LieDerivation.ad LieSubalgebra.lieRing LieSubalgebra.lieAlgebra	—	LieEquiv.isKilling lieAlgebraSelfModule LieDerivation.injective_ad_of_center_eq_bot LieAlgebra.center_eq_bot LieAlgebra.instIsFaithfulOfHasTrivialRadical LieAlgebra.IsKilling.instHasTrivialRadical Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
killingForm_restrict_range_ad 📖	mathematical	—	LinearMap.BilinForm.restrict LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieDerivation.instLieRing LieDerivation.instLieAlgebra killingForm LieSubalgebra.toSubmodule LieHom.range LieDerivation.ad LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra	—	lieAlgebraSelfModule LieHom.IsIdealMorphism.eq LieDerivation.ad_isIdealMorphism LieIdeal.killingForm_eq Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite LieDerivation.instNoetherian isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian Module.Projective.of_free Module.Free.of_divisionRing instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
killingForm_restrict_range_ad_nondegenerate 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieDerivation.instLieRing LieDerivation.instLieAlgebra SetLike.instMembership Submodule.setLike LieSubalgebra.toSubmodule LieHom.range LieDerivation.ad Submodule.addCommMonoid Submodule.module LinearMap.BilinForm.restrict killingForm	—	lieAlgebraSelfModule killingForm_restrict_range_ad LieAlgebra.IsKilling.killingForm_nondegenerate instIsKilling_range_ad
rangeAdOrthogonal_carrier 📖	mathematical	—	SetLike.coe LieSubmodule LieDerivation EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule LieDerivation.instAddCommGroup LieDerivation.instModule CommSemiring.toSemiring CommRing.toCommSemiring smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LieDerivation.instSMulBase LieDerivation.instLieRingModule LieSubmodule.instSetLike rangeAdOrthogonal setOf	—	RingHomSurjective.ids
range_ad_eq_top 📖	mathematical	—	LieHom.range EuclideanDomain.toCommRing Field.toEuclideanDomain LieDerivation LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule lieAlgebraSelfModule LieDerivation.instLieRing LieDerivation.instLieAlgebra LieDerivation.ad Top.top LieSubalgebra LieSubalgebra.instTop	—	lieAlgebraSelfModule LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite LieDerivation.instNoetherian isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors smulCommClass_self LieDerivation.instSMulBase LinearMap.IsSymm.isRefl LieModule.traceForm_isSymm killingForm_restrict_range_ad_nondegenerate Submodule.eq_bot_iff LieDerivation.ext RingHomSurjective.ids Submodule.map.congr_simp LieAlgebra.IsKilling.ker_killingForm_eq_bot instIsKilling_range_ad Submodule.map_bot ad_mem_ker_killingForm_ad_range_of_mem_orthogonal

---

← Back to Index