Documentation Verification Report

DirectSum

📁 Source: Mathlib/LinearAlgebra/Multilinear/DirectSum.lean

Statistics

Metric	Count
Definitions `fromDirectSumEquiv`	1
Theorems `directSum_ext`, `directSum_ext_iff`, `fromDirectSumEquiv_apply`, `fromDirectSumEquiv_lof`, `fromDirectSumEquiv_symm_apply`	5
Total	6

MultilinearMap

Definitions

Name	Category	Theorems
`fromDirectSumEquiv` 📖	CompOp	3 math math: `fromDirectSumEquiv_symm_apply`, `fromDirectSumEquiv_lof`, `fromDirectSumEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directSum_ext` 📖	—	`compLinearMap` `DirectSum` `CommSemiring.toSemiring` `instAddCommMonoidDirectSum` `DirectSum.instModule` `DirectSum.lof`	—	—	`dfinsupp_ext`
`directSum_ext_iff` 📖	mathematical	—	`compLinearMap` `DirectSum` `CommSemiring.toSemiring` `instAddCommMonoidDirectSum` `DirectSum.instModule` `DirectSum.lof`	—	`directSum_ext`
`fromDirectSumEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `DirectSum` `CommSemiring.toSemiring` `instAddCommMonoidDirectSum` `DirectSum.instModule` `instFunLikeForall` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `addCommMonoid` `Pi.module` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `fromDirectSumEquiv` `Finite.of_fintype` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFinsupp.instDFunLike` `Finset.sum` `Fintype.piFinset` `DFinsupp.support`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `fromDirectSumEquiv.eq_1` `fromDFinsuppEquiv_apply` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`fromDirectSumEquiv_lof` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `DirectSum` `CommSemiring.toSemiring` `instAddCommMonoidDirectSum` `DirectSum.instModule` `instFunLikeForall` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `addCommMonoid` `Pi.module` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `fromDirectSumEquiv` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof`	—	`RingHomInvPair.ids` `smulCommClass_self` `fromDirectSumEquiv.eq_1` `fromDFinsuppEquiv_single` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`fromDirectSumEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MultilinearMap` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `addCommMonoid` `Pi.addCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Pi.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `fromDirectSumEquiv` `compLinearMap` `DirectSum.lof`	—	`RingHomInvPair.ids` `smulCommClass_self` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`

---

← Back to Index