Projective

📁 Source: Mathlib/RingTheory/Finiteness/Projective.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_comp_eq_id_of_projective	1
Total	1

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_comp_eq_id_of_projective 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids LinearMap.id	—	RingHomCompTriple.ids exists_fin' Module.projective_lifting_property LinearMap.injective_of_comp_eq_id RingHomInvPair.ids

---

← Back to Index