Documentation Verification Report

ProjectiveDimension

📁 Source: Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean

Statistics

Metric	Count
Definitions	0
Theorems `hasProjectiveDimensionLE_of_linearEquiv`, `hasProjectiveDimensionLE_of_semiLinearEquiv`, `projectiveDimension_eq_of_linearEquiv`, `projectiveDimension_eq_of_semiLinearEquiv`	4
Total	4

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProjectiveDimensionLE_of_linearEquiv` 📖	mathematical	—	`HasProjectiveDimensionLE` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.abelian`	—	`RingHomInvPair.ids` `hasProjectiveDimensionLE_of_semiLinearEquiv`
`hasProjectiveDimensionLE_of_semiLinearEquiv` 📖	mathematical	—	`HasProjectiveDimensionLE` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.abelian`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHomInvPair.of_ringEquiv` `zero_add` `projective_iff_hasProjectiveDimensionLT_one` `IsProjective.iff_projective` `Module.Projective.of_equiv` `ModuleCat.shortExact_projectiveShortComplex` `RingHomCompTriple.right_ids` `RingHomCompTriple.ids` `RingHomInvPair.ids` `RingHomInvPair.symm` `Finsupp.lhom_ext'` `LinearMap.ext` `Finsupp.mapDomain_single` `Finsupp.mapRange_single` `LinearEquiv.map_zero` `Module.Basis.constr_apply` `Equiv.symm_apply_apply` `Finsupp.sum_single_index` `zero_smul` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.ker_comp` `LinearEquiv.ker_comp` `RingHomSurjective.invPair` `Submodule.comap_equiv_eq_map_symm` `ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff` `ModuleCat.projective_of_categoryTheory_projective` `Module.Projective.of_free` `instFreeCarrierX₂ModuleCatProjectiveShortComplex`
`projectiveDimension_eq_of_linearEquiv` 📖	mathematical	—	`projectiveDimension` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.abelian`	—	`RingHomInvPair.ids` `projectiveDimension_eq_of_semiLinearEquiv`
`projectiveDimension_eq_of_semiLinearEquiv` 📖	mathematical	—	`projectiveDimension` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.abelian`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHomInvPair.of_ringEquiv` `eq_of_forall_ge_iff` `Equiv.subsingleton_congr` `hasProjectiveDimensionLE_of_semiLinearEquiv`

---

← Back to Index