Injective

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

Statistics

Metric	Count
Definitions	0
Theorems injective_as_module_iff, injective_of_divisible, of_divisible	3
Total	3

AddCommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_as_module_iff 📖	mathematical	—	CategoryTheory.Injective ModuleCat Int.instRing ModuleCat.moduleCategory ModuleCat.of AddCommGroup.toIntModule AddCommGrpCat instCategory of	—	ModuleCat.forget₂AddCommGroupIsEquivalence CategoryTheory.Equivalence.map_injective_iff
injective_of_divisible 📖	mathematical	—	CategoryTheory.Injective AddCommGrpCat instCategory of	—	injective_as_module_iff Module.injective_object_of_injective_module Module.Baer.injective Module.Baer.of_divisible

Module.Baer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_divisible 📖	mathematical	—	Module.Baer Int.instRing AddCommGroup.toIntModule	—	IsPrincipalIdealRing.principal EuclideanDomain.to_principal_ideal_domain eq_or_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Submodule.span_zero_singleton Submodule.subset_span Set.mem_singleton Submodule.mem_span_singleton map_zsmul LinearMap.toSpanSingleton_apply DivisibleBy.div_cancel SMulMemClass.smul_mem Submodule.smulMemClass

---

← Back to Index