Documentation Verification Report

Derivation

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

Statistics

Metric	Count
Definitions `ad`	1
Theorems `ad_apply_apply`, `ad_apply_lieDerivation`, `ad_isIdealMorphism`, `ad_ker_eq_center`, `coe_ad_apply_eq_ad_apply`, `injective_ad_of_center_eq_bot`, `lie_ad`, `lie_der_ad_eq_ad_der`, `maxTrivSubmodule_eq_bot_of_center_eq_bot`, `mem_ad_idealRange_iff`	10
Total	11

LieDerivation

Definitions

Name	Category	Theorems
`ad` 📖	CompOp	17 math math: `IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal`, `lie_der_ad_eq_ad_der`, `ad_apply_lieDerivation`, `IsKilling.instIsKilling_range_ad`, `IsKilling.exists_eq_ad`, `IsKilling.killingForm_restrict_range_ad`, `IsKilling.ad_mem_orthogonal_of_mem_orthogonal`, `ad_isIdealMorphism`, `IsKilling.range_ad_eq_top`, `lie_ad`, `IsKilling.ad_apply_eq_zero_iff`, `injective_ad_of_center_eq_bot`, `coe_ad_apply_eq_ad_apply`, `ad_ker_eq_center`, `mem_ad_idealRange_iff`, `IsKilling.killingForm_restrict_range_ad_nondegenerate`, `ad_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ad_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instFunLike` `LieHom` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `ad` `Bracket.bracket` `LieRingModule.toBracket`	—	`lie_skew`
`ad_apply_lieDerivation` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `ad` `instFunLike` `instNeg` `Bracket.bracket` `LieRingModule.toBracket` `instAddCommGroup` `instLieRingModule`	—	`lieAlgebraSelfModule`
`ad_isIdealMorphism` 📖	mathematical	—	`LieHom.IsIdealMorphism` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instLieRing` `instLieAlgebra` `ad`	—	`lieAlgebraSelfModule` `lie_der_ad_eq_ad_der`
`ad_ker_eq_center` 📖	mathematical	—	`LieHom.ker` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instLieRing` `instLieAlgebra` `ad` `LieAlgebra.center`	—	`LieSubmodule.ext` `lieAlgebraSelfModule` `LieAlgebra.self_module_ker_eq_center` `LieHom.mem_ker` `LieModule.mem_ker` `ad_apply_apply`
`coe_ad_apply_eq_ad_apply` 📖	mathematical	—	`toLinearMap` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `DFunLike.coe` `LieHom` `LieDerivation` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `ad` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `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` `LieAlgebra.ad`	—	`LinearMap.ext` `lieAlgebraSelfModule` `smulCommClass_self` `IsScalarTower.left` `ad_apply_apply`
`injective_ad_of_center_eq_bot` 📖	mathematical	`LieAlgebra.center` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	`LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `DFunLike.coe` `LieHom` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `ad`	—	`lieAlgebraSelfModule` `LieHom.ker_eq_bot` `ad_ker_eq_center`
`lie_ad` 📖	mathematical	—	`Bracket.bracket` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instBracket` `DFunLike.coe` `LieHom` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `ad` `LieRingModule.toBracket` `instAddCommGroup` `instLieRingModule`	—	`lieAlgebraSelfModule` `ext` `ad_apply_apply` `apply_lie_eq_sub` `sub_sub_cancel`
`lie_der_ad_eq_ad_der` 📖	mathematical	—	`Bracket.bracket` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instBracket` `DFunLike.coe` `LieHom` `instLieRing` `instLieAlgebra` `LieHom.instFunLike` `ad` `instFunLike`	—	`lieAlgebraSelfModule` `ad_apply_lieDerivation` `lie_ad` `lie_skew`
`maxTrivSubmodule_eq_bot_of_center_eq_bot` 📖	mathematical	`LieAlgebra.center` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	`LieModule.maxTrivSubmodule` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `instAddCommGroup` `instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instSMulBase` `instLieRingModule` `instLieModule` `Bot.bot` `LieSubmodule` `LieSubmodule.instBot`	—	`lieAlgebraSelfModule` `smulCommClass_self` `instSMulBase` `instLieModule` `LieSubmodule.eq_bot_iff` `ext` `LieModule.mem_maxTrivSubmodule` `neg_zero` `LieSubmodule.mem_bot` `ad_ker_eq_center` `LieHom.mem_ker`
`mem_ad_idealRange_iff` 📖	mathematical	—	`LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieIdeal` `instLieRing` `instLieAlgebra` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieHom.idealRange` `ad` `DFunLike.coe` `LieHom` `LieHom.instFunLike`	—	`lieAlgebraSelfModule` `LieHom.mem_idealRange_iff` `ad_isIdealMorphism`

---

← Back to Index