Documentation Verification Report

FiniteDimensional

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

Statistics

Metric	Count
Definitions	0
Theorems `multilinearMap`, `multilinearMap`	2
Total	2

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multilinearMap` 📖	mathematical	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.Free`	`MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self`

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multilinearMap` 📖	mathematical	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.Free`	`MultilinearMap` `MultilinearMap.addCommMonoid` `MultilinearMap.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self`

---

← Back to Index