Documentation Verification Report

DirectSum

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

Statistics

Metric	Count
Definitions `instLieRingModule`, `lieAlgebra`, `lieAlgebraComponent`, `lieAlgebraOf`, `lieAlgebraOfIdeals`, `lieModuleComponent`, `lieModuleOf`, `lieRing`, `lieRingOfIdeals`, `toLieAlgebra`	10
Theorems `bracket_apply`, `instLieModule`, `lieAlgebraComponent_apply`, `lieAlgebraOf_apply`, `lieAlgebra_ext`, `lie_module_bracket_apply`, `lie_of`, `lie_of_of_ne`, `lie_of_same`, `toLieAlgebra_apply`	10
Total	20

DirectSum

Definitions

Name	Category	Theorems
`instLieRingModule` 📖	CompOp	2 math math: `lie_module_bracket_apply`, `instLieModule`
`lieAlgebra` 📖	CompOp	3 math math: `lieAlgebraComponent_apply`, `lieAlgebraOf_apply`, `toLieAlgebra_apply`
`lieAlgebraComponent` 📖	CompOp	1 math math: `lieAlgebraComponent_apply`
`lieAlgebraOf` 📖	CompOp	1 math math: `lieAlgebraOf_apply`
`lieAlgebraOfIdeals` 📖	CompOp	—
`lieModuleComponent` 📖	CompOp	—
`lieModuleOf` 📖	CompOp	—
`lieRing` 📖	CompOp	7 math math: `bracket_apply`, `lie_of_of_ne`, `lie_of`, `lieAlgebraComponent_apply`, `lieAlgebraOf_apply`, `lie_of_same`, `toLieAlgebra_apply`
`lieRingOfIdeals` 📖	CompOp	—
`toLieAlgebra` 📖	CompOp	1 math math: `toLieAlgebra_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bracket_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Bracket.bracket` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieRingModule.toBracket` `lieRing` `lieRingSelfModule`	—	`DFinsupp.zipWith_apply`
`instLieModule` 📖	mathematical	`LieModule`	`DirectSum` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instLieRingModule`	—	`ext` `lie_module_bracket_apply` `smul_lie` `smul_apply` `lie_smul`
`lieAlgebraComponent_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `lieRing` `lieAlgebra` `LieHom.instFunLike` `lieAlgebraComponent` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum` `instModule` `LieAlgebra.toModule` `LinearMap.instFunLike` `component`	—	—
`lieAlgebraOf_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `lieRing` `lieAlgebra` `LieHom.instFunLike` `lieAlgebraOf` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	—
`lieAlgebra_ext` 📖	—	`DFunLike.coe` `LieHom` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `lieRing` `lieAlgebra` `LieHom.instFunLike` `lieAlgebraComponent`	—	—	`DFinsupp.ext`
`lie_module_bracket_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Bracket.bracket` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRingModule.toBracket` `instAddCommGroup` `instLieRingModule`	—	`DFinsupp.mapRange_apply`
`lie_of` 📖	mathematical	—	`Bracket.bracket` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieRingModule.toBracket` `lieRing` `lieRingSelfModule` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup`	—	`Decidable.eq_or_ne` `lie_of_same` `lie_of_of_ne`
`lie_of_of_ne` 📖	mathematical	—	`Bracket.bracket` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieRingModule.toBracket` `lieRing` `lieRingSelfModule` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup`	—	`ext` `bracket_apply` `Decidable.eq_or_ne` `of_eq_of_ne` `lie_zero` `zero_apply` `zero_lie`
`lie_of_same` 📖	mathematical	—	`Bracket.bracket` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieRingModule.toBracket` `lieRing` `lieRingSelfModule` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`DFinsupp.zipWith_single_single`
`toLieAlgebra_apply` 📖	mathematical	`Pairwise`	`DFunLike.coe` `LieHom` `DirectSum` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `lieRing` `lieAlgebra` `LieHom.instFunLike` `toLieAlgebra` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum` `instModule` `LieAlgebra.toModule` `LinearMap.instFunLike` `toModule` `LieHom.toLinearMap`	—	—

---

← Back to Index