Documentation Verification Report

Lie

📁 Source: Mathlib/RingTheory/Derivation/Lie.lean

Statistics

Metric	Count
Definitions `instBracket`, `instLieAlgebra`, `instLieRing`, `instLieRingModule`	4
Theorems `bracket_eq_fun`, `commutator_apply`, `commutator_coe_linear_map`, `instLieModule`	4
Total	8

Derivation

Definitions

Name	Category	Theorems
`instBracket` 📖	CompOp	3 math math: `commutator_coe_linear_map`, `commutator_apply`, `LeftInvariantDerivation.commutator_coe_derivation`
`instLieAlgebra` 📖	CompOp	3 math math: `LieRinehartAlgebra.Hom.anchor_derivation`, `instLieModule`, `LieRinehartAlgebra.instDerivation`
`instLieRing` 📖	CompOp	5 math math: `LieRinehartAlgebra.Hom.anchor_derivation`, `bracket_eq_fun`, `instLieModule`, `LieRinehartAlgebra.instDerivation`, `LieRinehartAlgebra.instLieRinehartRingDerivation`
`instLieRingModule` 📖	CompOp	5 math math: `LieRinehartAlgebra.Hom.anchor_derivation`, `bracket_eq_fun`, `instLieModule`, `LieRinehartAlgebra.instDerivation`, `LieRinehartAlgebra.instLieRinehartRingDerivation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bracket_eq_fun` 📖	mathematical	—	`Bracket.bracket` `Derivation` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `LieRingModule.toBracket` `instLieRing` `LieRing.toAddCommGroup` `instLieRingModule` `DFunLike.coe` `instFunLike`	—	—
`commutator_apply` 📖	mathematical	—	`DFunLike.coe` `Derivation` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `instFunLike` `Bracket.bracket` `instBracket` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	—
`commutator_coe_linear_map` 📖	mathematical	—	`toLinearMap` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `Bracket.bracket` `Derivation` `instBracket` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LieRingModule.toBracket` `Module.End.instRing` `LieRing.toAddCommGroup` `LinearMap.addCommGroup` `AddCommGroup.toAddCommMonoid` `LinearMap.instLieRingModule` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.End.instLieRingModule` `Module.End.instLieModule`	—	—
`instLieModule` 📖	mathematical	—	`LieModule` `Derivation` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `instLieRing` `instLieAlgebra` `LieRing.toAddCommGroup` `instLieRingModule`	—	`map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.left`

---

← Back to Index