TraceForm

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

Statistics

Metric	Count
Definitions `killingCompl`, `traceForm`, `killingForm`	3
Theorems `coe_killingCompl_top`, `killingForm_eq`, `le_killingCompl_top_of_isLieAbelian`, `mem_killingCompl`, `restrict_killingForm`, `toSubmodule_killingCompl`, `eq_zero_of_mem_genWeightSpace_mem_posFitting`, `isLieAbelian_of_ker_traceForm_eq_bot`, `lie_traceForm_eq_zero`, `lowerCentralSeries_one_inf_center_le_ker_traceForm`, `range_traceForm_le_span_weight`, `traceForm_apply_apply`, `traceForm_apply_eq_zero_of_mem_lcs_of_mem_center`, `traceForm_apply_lie_apply`, `traceForm_apply_lie_apply'`, `traceForm_comm`, `traceForm_eq_sum_finrank_nsmul`, `traceForm_eq_sum_finrank_nsmul'`, `traceForm_eq_sum_finrank_nsmul_mul`, `traceForm_eq_sum_genWeightSpaceOf`, `traceForm_eq_zero_if_mem_lcs_of_mem_ucs`, `traceForm_eq_zero_of_isNilpotent`, `traceForm_eq_zero_of_isTrivial`, `traceForm_flip`, `traceForm_genWeightSpace_eq`, `traceForm_isSymm`, `traceForm_lieInvariant`, `traceForm_lieSubalgebra_mk_left`, `traceForm_lieSubalgebra_mk_right`, `trace_toEnd_eq_zero_of_mem_lcs`, `traceForm_eq_of_le_idealizer`, `traceForm_eq_zero_of_isTrivial`, `trace_eq_trace_restrict_of_le_idealizer`, `killingForm_apply_apply`, `killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting`	35
Total	38

LieIdeal

Definitions

Name	Category	Theorems
`killingCompl` 📖	CompOp	6 math math: `coe_killingCompl_top`, `mem_killingCompl`, `le_killingCompl_top_of_isLieAbelian`, `isCompl_killingCompl`, `LieAlgebra.IsKilling.killingCompl_top_eq_bot`, `toSubmodule_killingCompl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_killingCompl_top` 📖	mathematical	—	`LieSubalgebra.toSubmodule` `toLieSubalgebra` `killingCompl` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LinearMap.ker` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm`	—	`Submodule.ext` `lieAlgebraSelfModule` `LieModule.traceForm_comm`
`killingForm_eq` 📖	mathematical	—	`killingForm` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `LinearMap.BilinForm.restrict` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.toSubmodule` `toLieSubalgebra`	—	`LieSubmodule.traceForm_eq_of_le_idealizer` `lieAlgebraSelfModule` `idealizer_eq_normalizer`
`le_killingCompl_top_of_isLieAbelian` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `killingCompl` `Top.top` `LieSubmodule.instTop`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `smulCommClass_self` `RingHomCompTriple.ids` `IsScalarTower.left` `lieAlgebraSelfModule` `LieModule.traceForm_apply_apply` `LieSubmodule.traceForm_eq_zero_of_isTrivial` `idealizer_eq_normalizer`
`mem_killingCompl` 📖	mathematical	—	`LieIdeal` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `killingCompl` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`restrict_killingForm` 📖	mathematical	—	`LinearMap.BilinForm.restrict` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `killingForm` `LieSubalgebra.toSubmodule` `toLieSubalgebra` `LieModule.traceForm` `LieSubmodule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `lieRingModule` `lieModule` `lieAlgebraSelfModule`	—	—
`toSubmodule_killingCompl` 📖	mathematical	—	`LieSubmodule.toSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `killingCompl` `LinearMap.BilinForm.orthogonal` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `killingForm`	—	—

LieModule

Definitions

Name	Category	Theorems
`traceForm` 📖	CompOp	29 math math: `LieIdeal.restrict_killingForm`, `traceForm_eq_sum_genWeightSpaceOf`, `traceForm_eq_sum_finrank_nsmul'`, `LieAlgebra.IsKilling.traceForm_cartan_nondegenerate`, `lowerCentralSeries_one_inf_center_le_ker_traceForm`, `LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra`, `traceForm_eq_zero_of_isNilpotent`, `LieSubmodule.traceForm_eq_of_le_idealizer`, `traceForm_isSymm`, `traceForm_lieSubalgebra_mk_right`, `traceForm_comm`, `lie_traceForm_eq_zero`, `traceForm_eq_zero_of_isTrivial`, `traceForm_eq_zero_if_mem_lcs_of_mem_ucs`, `traceForm_eq_sum_finrank_nsmul`, `traceForm_lieSubalgebra_mk_left`, `LieAlgebra.restrict_killingForm`, `LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker`, `traceForm_genWeightSpace_eq`, `traceForm_apply_apply`, `traceForm_apply_lie_apply`, `LieAlgebra.IsKilling.traceForm_coroot`, `traceForm_eq_sum_finrank_nsmul_mul`, `LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot`, `traceForm_apply_eq_zero_of_mem_lcs_of_mem_center`, `traceForm_flip`, `traceForm_apply_lie_apply'`, `range_traceForm_le_span_weight`, `traceForm_lieInvariant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_mem_genWeightSpace_mem_posFitting` 📖	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `Bracket.bracket` `LieRingModule.toBracket` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `genWeightSpace` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `posFittingComp`	—	—	`smulCommClass_self` `IsScalarTower.left` `pow_zero` `one_mul` `mul_neg` `neg_mul` `neg_neg` `pow_succ` `smul_eq_mul` `RingHomCompTriple.ids` `Module.End.mul_eq_comp` `LinearMap.comp_apply` `pow_succ'` `smul_assoc` `IsScalarTower.right` `zero_smul` `sub_zero` `mem_posFittingCompOf` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `MulZeroClass.mul_zero` `LieSubmodule.iSup_induction` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero`
`isLieAbelian_of_ker_traceForm_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` `traceForm` `Bot.bot` `Submodule` `Submodule.instBot`	`IsLieAbelian` `LieRingModule.toBracket` `lieRingSelfModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`lieAlgebraSelfModule` `disjoint_lowerCentralSeries_maxTrivSubmodule_iff` `lowerCentralSeries_one_inf_center_le_ker_traceForm`
`lie_traceForm_eq_zero` 📖	mathematical	—	`Bracket.bracket` `LinearMap.BilinForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieRingModule.toBracket` `LinearMap.addCommGroup` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LinearMap.module` `LinearMap.instLieRingModule` `lieRingSelfModule` `lieAlgebraSelfModule` `Module.Dual.instLieRingModule` `Module.Dual.instLieModule` `traceForm` `LinearMap.instZero` `LinearMap.addCommMonoid`	—	`LinearMap.BilinForm.ext` `lieAlgebraSelfModule` `Module.Dual.instLieModule` `LieHom.lie_apply` `LinearMap.sub_apply` `Module.Dual.lie_apply` `LinearMap.zero_apply` `traceForm_apply_lie_apply'` `sub_self`
`lowerCentralSeries_one_inf_center_le_ker_traceForm` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `LieSubmodule` `lieRingSelfModule` `LieSubmodule.instMin` `lowerCentralSeries` `LieAlgebra.center` `LinearMap.ker` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm`	—	`LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `IsScalarTower.left` `traceForm_apply_apply` `LinearMap.zero_apply` `Algebra.to_smulCommClass` `LinearMap.trace_baseChange` `LinearMap.baseChange_comp` `LieAlgebra.ExtendScalars.instLieModule` `toEnd_baseChange` `lieAlgebraSelfModule` `lowerCentralSeries_succ` `LieSubmodule.baseChange_top` `LieSubmodule.lie_baseChange` `Submodule.tmul_mem_baseChange_of_mem` `TensorProduct.induction_on` `mul_one` `TensorProduct.tmul_zero` `add_lie` `add_zero` `LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Algebra.TensorProduct.instFree` `Module.Finite.base_change` `commute_toEnd_of_mem_center_right` `IsTriangularizable.maxGenEigenspace_eq_top` `instIsTriangularizableOfIsAlgClosed` `AlgebraicClosure.isAlgClosed` `trace_toEnd_eq_zero_of_mem_lcs` `instIsNilpotentTensor` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `le_refl` `Module.IsTorsionFree.trans_faithfulSMul` `FractionRing.instFaithfulSMul` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `IsDomain.toIsCancelMulZero` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`range_traceForm_le_span_weight` 📖	mathematical	—	`Submodule` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHomSurjective.ids` `traceForm` `Submodule.span` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Set.range` `Weight` `Weight.toLinear`	—	`RingHomSurjective.ids` `Algebra.to_smulCommClass` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `traceForm_eq_sum_finrank_nsmul` `LinearMap.coe_sum` `Finset.sum_apply` `Submodule.sum_mem` `AddMonoid.nat_smulCommClass'` `Nat.cast_smul_eq_nsmul` `Submodule.smul_mem` `Submodule.subset_span` `Set.mem_range_self`
`traceForm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.trace` `LinearMap.comp` `RingHomCompTriple.ids` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `toEnd`	—	—
`traceForm_apply_eq_zero_of_mem_lcs_of_mem_center` 📖	mathematical	`LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lowerCentralSeries` `LieIdeal` `LieAlgebra.center`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`traceForm_eq_zero_if_mem_lcs_of_mem_ucs` `LieIdeal.lcs_succ` `lowerCentralSeries_succ` `lieAlgebraSelfModule` `LieSubmodule.ucs_succ`
`traceForm_apply_lie_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `Bracket.bracket` `LieRingModule.toBracket` `lieRingSelfModule`	—	`smulCommClass_self` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.comp.congr_simp` `LieHom.map_lie` `sub_mul` `mul_assoc` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.trace_mul_cycle'` `mul_sub`
`traceForm_apply_lie_apply'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `Bracket.bracket` `LieRingModule.toBracket` `lieRingSelfModule` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `CommRing.toRing`	—	`lie_skew` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.neg_apply` `traceForm_apply_lie_apply`
`traceForm_comm` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm`	—	`LinearMap.trace_mul_comm` `smulCommClass_self` `IsScalarTower.left`
`traceForm_eq_sum_finrank_nsmul` 📖	mathematical	—	`traceForm` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.sum` `Weight` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `LinearMap.addCommMonoid` `LinearMap.module` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Field.toSemifield` `Finset.univ` `Weight.instFintype` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `AddMonoid.toNatSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LinearMap.addCommGroup` `Module.finrank` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `genWeightSpace` `DFunLike.coe` `Weight.instFunLike` `DivisionSemiring.toSemiring` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `LieSubmodule.instSMulMemClass` `LinearMap.smulRight` `LinearMap.instIsScalarTower` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.right` `Weight.toLinear`	—	`LinearMap.BilinForm.ext` `Algebra.to_smulCommClass` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `traceForm_eq_sum_finrank_nsmul_mul` `Finset.sum_attach` `Finset.mem_univ` `Finset.sum_congr` `nsmul_eq_mul` `Finset.sum_attach_univ` `AddMonoid.nat_smulCommClass'` `LinearMap.coe_sum` `Finset.sum_apply`
`traceForm_eq_sum_finrank_nsmul'` 📖	mathematical	—	`traceForm` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.sum` `Weight` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `LinearMap.addCommMonoid` `LinearMap.module` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Field.toSemifield` `Finset.filter` `Weight.IsNonZero` `Weight.instDecidablePredIsNonZero` `Finset.univ` `Weight.instFintype` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `AddMonoid.toNatSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LinearMap.addCommGroup` `Module.finrank` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `genWeightSpace` `DFunLike.coe` `Weight.instFunLike` `DivisionSemiring.toSemiring` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `LieSubmodule.instSMulMemClass` `LinearMap.smulRight` `LinearMap.instIsScalarTower` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.right` `Weight.toLinear`	—	`Algebra.to_smulCommClass` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `Finset.sum_eq_zero` `Finset.filter.congr_simp` `LinearMap.smulRight.congr_simp` `LinearMap.smulRight_zero` `nsmul_zero` `traceForm_eq_sum_finrank_nsmul` `Finset.sum_filter_add_sum_filter_not` `Finset.sum_congr` `add_zero`
`traceForm_eq_sum_finrank_nsmul_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `Finset.sum` `Weight` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `Weight.instFintype` `instIsDomain` `Field.toSemifield` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Ring.toSemiring` `instIsSimpleModule` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Module.finrank` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `genWeightSpace` `Weight.instFunLike` `DivisionSemiring.toSemiring` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `AddCommGroup.toAddGroup` `LieSubmodule.instSMulMemClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `LieSubmodule.lie_mem` `Submodule.addSubmonoidClass` `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` `LieSubmodule.iSupIndep_toSubmodule` `iSupIndep_genWeightSpace'` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieSubmodule.iSup_toSubmodule_eq_top` `iSup_genWeightSpace_eq_top'` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LinearMap.trace_eq_sum_trace_restrict` `FiniteDimensional.finiteDimensional_submodule` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ideal.instIsTorsionFreeSubtypeMemSubmodule` `LieSubmodule.instLieModule` `Finset.sum_congr` `traceForm_genWeightSpace_eq`
`traceForm_eq_sum_genWeightSpaceOf` 📖	mathematical	—	`traceForm` `Finset.sum` `LinearMap.BilinForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.addCommMonoid` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Set.Finite.toFinset` `setOf` `LieSubmodule` `genWeightSpaceOf` `Bot.bot` `LieSubmodule.instBot` `finite_genWeightSpaceOf_ne_bot` `SetLike.instMembership` `LieSubmodule.instSetLike` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `AddCommGroup.toAddGroup` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieRingModuleSubtypeMem` `LieSubmodule.instLieModule`	—	`LinearMap.BilinForm.ext` `finite_genWeightSpaceOf_ne_bot` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `LieSubmodule.lie_mem` `LieSubmodule.toSubmodule_eq_bot` `LieSubmodule.iSupIndep_toSubmodule` `iSupIndep_genWeightSpaceOf` `Submodule.addSubmonoidClass` `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` `iSup_genWeightSpaceOf_eq_top` `LinearMap.trace_eq_sum_trace_restrict'` `Module.IsNoetherian.finite` `isNoetherian_submodule'` `Module.free_of_finite_type_torsion_free'` `Ideal.instIsTorsionFreeSubtypeMemSubmodule` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_congr` `Set.Finite.toFinset.congr_simp`
`traceForm_eq_zero_if_mem_lcs_of_mem_ucs` 📖	mathematical	`LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal.lcs` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieSubmodule.ucs` `lieAlgebraSelfModule` `Bot.bot` `LieSubmodule.instBot`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`lieAlgebraSelfModule` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Submodule.span_induction` `lie_skew` `map_neg` `LinearMap.neg_apply` `neg_eq_zero` `traceForm_apply_lie_apply` `LieSubmodule.mem_normalizer` `LieSubmodule.ucs_succ` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero` `Algebra.to_smulCommClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `MulZeroClass.mul_zero` `LieSubmodule.lieIdeal_oper_eq_linear_span'` `LieIdeal.lcs_succ`
`traceForm_eq_zero_of_isNilpotent` 📖	mathematical	—	`traceForm` `LinearMap.BilinForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module`	—	`LinearMap.BilinForm.ext` `smulCommClass_self` `RingHomCompTriple.ids` `IsScalarTower.left` `LinearMap.isNilpotent_trace_of_isNilpotent` `isNilpotent_toEnd_of_isNilpotent₂`
`traceForm_eq_zero_of_isTrivial` 📖	mathematical	—	`traceForm` `LinearMap.BilinForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module`	—	`LinearMap.BilinForm.ext` `RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `LinearMap.ext` `trivial_lie_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`traceForm_flip` 📖	mathematical	—	`LinearMap.flip` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `RingHom.id` `traceForm`	—	`SMulCommClass.symm` `LinearMap.ext₂` `traceForm_comm`
`traceForm_genWeightSpace_eq` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `genWeightSpace` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `AddCommGroup.toAddGroup` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieRingModuleSubtypeMem` `LieSubmodule.instLieModule` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Module.finrank` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `nsmul_eq_mul` `mul_comm` `sub_self` `mul_left_comm` `shiftedGenWeightSpace.instSubtypeMemLieSubmodule` `traceForm_eq_zero_of_isNilpotent` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian` `LinearMap.congr_fun` `sub_eq_zero` `sub_zero` `smulCommClass_self` `RingHomCompTriple.ids` `IsScalarTower.left` `traceForm_apply_apply` `LinearMap.trace_id` `Module.free_of_finite_type_torsion_free'` `Module.IsNoetherian.finite` `LieSubmodule.instIsNoetherianSubtypeMem` `LieSubmodule.instIsTorsionFreeSubtypeMem` `Module.IsReflexive.to_isTorsionFree` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `RingHomCompTriple.right_ids` `LinearMap.id_comp` `LinearMap.smul_comp` `LinearMap.comp_smul` `LinearMap.IsScalarTower.compatibleSMul` `trace_toEnd_genWeightSpace` `LinearMap.comp_id` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.sub_comp` `LinearMap.comp_sub` `RingHomInvPair.ids` `LinearMap.trace_conj'` `LinearEquiv.conj_comp` `shiftedGenWeightSpace.toEnd_eq` `LinearMap.zero_apply`
`traceForm_isSymm` 📖	mathematical	—	`LinearMap.IsSymm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `traceForm`	—	`traceForm_comm`
`traceForm_lieInvariant` 📖	mathematical	—	`LinearMap.BilinForm.lieInvariant` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `traceForm`	—	`lie_skew` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.neg_apply` `traceForm_apply_lie_apply`
`traceForm_lieSubalgebra_mk_left` 📖	mathematical	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `LieSubalgebra.lieRingModule` `LieSubalgebra.lieModule`	—	`LieSubalgebra.lieModule`
`traceForm_lieSubalgebra_mk_right` 📖	mathematical	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `traceForm` `LieSubalgebra.lieRingModule` `LieSubalgebra.lieModule`	—	`LieSubalgebra.lieModule`
`trace_toEnd_eq_zero_of_mem_lcs` 📖	mathematical	`LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lowerCentralSeries`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.trace` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `toEnd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`antitone_lowerCentralSeries` `LieSubmodule.lieIdeal_oper_eq_linear_span'` `lieAlgebraSelfModule` `LieSubmodule.mem_toSubmodule` `lowerCentralSeries_succ` `Submodule.span_induction` `smulCommClass_self` `IsScalarTower.left` `LieHom.map_lie` `LinearMap.trace_lie` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieHom.instLinearMapClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `MulZeroClass.mul_zero`

LieSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`traceForm_eq_of_le_idealizer` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `idealizer`	`LieModule.traceForm` `LieSubmodule` `SetLike.instMembership` `instSetLike` `LieIdeal.lieRing` `LieIdeal.lieAlgebra` `AddSubgroupClass.toAddCommGroup` `instAddSubgroupClass` `SubmoduleClass.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toAddGroup` `instSMulMemClass` `LieIdeal.lieRingModule` `instLieRingModuleSubtypeMem` `LieIdeal.lieModule` `instLieModule` `LinearMap.BilinForm.restrict` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra`	—	`LinearMap.BilinForm.ext` `instAddSubgroupClass` `instSMulMemClass` `LieIdeal.lieModule` `instLieModule` `smulCommClass_self` `RingHomCompTriple.ids` `IsScalarTower.left` `lie_mem` `mem_idealizer` `trace_eq_trace_restrict_of_le_idealizer`
`traceForm_eq_zero_of_isTrivial` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `idealizer` `SetLike.instMembership` `instSetLike`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.trace` `LinearMap.comp` `RingHomCompTriple.ids` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`instAddSubgroupClass` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `lie_mem` `mem_idealizer` `LinearMap.ext` `Submodule.coe_eq_zero` `LieModule.IsTrivial.trivial` `lie_zero` `instSMulMemClass` `trace_eq_trace_restrict_of_le_idealizer` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`trace_eq_trace_restrict_of_le_idealizer` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `idealizer` `SetLike.instMembership` `instSetLike` `lie_mem` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `mem_idealizer`	`LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `CommSemiring.toCommMonoid` `Semiring.toModule` `LinearMap.trace` `LinearMap.comp` `RingHomCompTriple.ids` `LieSubmodule` `AddSubgroupClass.toAddCommGroup` `instAddSubgroupClass` `SubmoduleClass.module` `AddCommGroup.toAddGroup` `instSMulMemClass` `LinearMap.restrict` `toSubmodule`	—	`RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `lie_mem` `instAddSubgroupClass` `instSMulMemClass` `LinearMap.trace_restrict_eq_of_forall_mem`

(root)

Definitions

Name	Category	Theorems
`killingForm` 📖	CompOp	19 math math: `LieAlgebra.IsKilling.restrict_killingForm_eq_sum`, `LieIdeal.restrict_killingForm`, `LieIdeal.coe_killingCompl_top`, `LieIdeal.mem_killingCompl`, `LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero`, `killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting`, `LieAlgebra.IsKilling.killingForm_nondegenerate`, `LieDerivation.IsKilling.killingForm_restrict_range_ad`, `LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing`, `killingForm_apply_apply`, `LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg`, `LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux`, `LieIdeal.killingForm_eq`, `LieAlgebra.restrict_killingForm`, `LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra`, `LieIdeal.toSubmodule_killingCompl`, `LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate`, `LieAlgebra.IsKilling.ker_killingForm_eq_bot`, `LieAlgebra.killingForm_of_equiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`killingForm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.trace` `LinearMap.comp` `RingHomCompTriple.ids` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieAlgebra.ad`	—	`LieModule.traceForm_apply_apply` `lieAlgebraSelfModule`
`killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting` 📖	mathematical	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieAlgebra.zeroRootSubalgebra` `LieSubmodule` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `LieModule.posFittingComp` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting` `LieModule.traceForm_apply_lie_apply'`

---

← Back to Index