Finite

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

Statistics

Metric	Count
Definitions	0
Theorems instDFinsupp, instDirectSum	2
Total	2

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDFinsupp 📖	mathematical	Module.Finite	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	equiv pi RingHomInvPair.ids
instDirectSum 📖	mathematical	Module.Finite	DirectSum instAddCommMonoidDirectSum DirectSum.instModule	—	instDFinsupp

---

← Back to Index