Finiteness

📁 Source: Mathlib/Algebra/Colimit/Finiteness.lean

Statistics

Metric	Count
Definitions fgSystem, equiv	2
Theorems equiv_comp_of, instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, instIsDirectedOrderSubtypeSubmoduleFG	3
Total	5

Module

Definitions

Name	Category	Theorems
fgSystem 📖	CompOp	2 math math: fgSystem.equiv_comp_of, fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId

Module.fgSystem

Definitions

Name	Category	Theorems
equiv 📖	CompOp	1 math math: equiv_comp_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_comp_of 📖	mathematical	—	LinearMap.comp Submodule SetLike.instMembership Submodule.setLike Submodule.FG Module.DirectLimit Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder Submodule.addCommMonoid Submodule.module Module.fgSystem Module.DirectLimit.addCommMonoid Module.DirectLimit.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids equiv Module.DirectLimit.of Submodule.subtype	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids Module.DirectLimit.lift_of
instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId 📖	mathematical	—	DirectedSystem Submodule Submodule.FG Subtype.preorder PartialOrder.toPreorder Submodule.instPartialOrder SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike Module.fgSystem	—	le_rfl
instIsDirectedOrderSubtypeSubmoduleFG 📖	mathematical	—	IsDirectedOrder Submodule Submodule.FG Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	—	Submodule.FG.sup Subtype.coe_le_coe le_sup_left le_sup_right

---

← Back to Index