Injective

📁 Source: MathlibTest/Algebra/Category/Grp/Injective.lean

Statistics

Metric	Count
Definitions Injective	1
Theorems Injective, Injective, Injective	3
Total	4

AddLECancellable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Injective 📖	—	AddLECancellable Preorder.toLE PartialOrder.toPreorder	—	—	le_antisymm Eq.le Eq.ge

FirstOrder.Language.LHom

Definitions

Name	Category	Theorems
Injective 📖	CompData	3 math math: sumInl_injective, FirstOrder.Language.lhomWithConstants_injective, sumInr_injective

FreeGroup.startsWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Injective 📖	mathematical	—	Set FreeGroup FreeGroup.startsWith	—	zero_add

MulLECancellable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Injective 📖	—	MulLECancellable Preorder.toLE PartialOrder.toPreorder	—	—	le_antisymm Eq.le Eq.ge

---

← Back to Index