Theorems · Theorem · category theory
ModuleCat.hom_ext
∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {f g : M ⟶ N}, ModuleCat.Hom.hom f = ModuleCat.Hom.hom g → f = g- Defined in
- Mathlib.Algebra.Category.ModuleCat.Basic
- Cited by
- 84 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Ringstatement and proof · cited by 7,463
- ModuleCatstatement and proof · cited by 1,429
- ModuleCat.carrierstatement · cited by 997
- ModuleCat.Hom.homstatement and proof · cited by 341
- ModuleCat.Hom.extproof · cited by 2
Cited by84
Results whose statement or proof uses this declaration.
- groupCohomology.comp_d₁₂_eqproof · cited by 10
- groupHomology.comp_d₂₁_eqproof · cited by 10
- ModuleCat.hom_ext_iffproof · cited by 10
- groupHomology.inhomogeneousChains.extproof · cited by 8
- groupCohomology.comp_d₀₁_eqproof · cited by 6
- groupHomology.comp_d₁₀_eqproof · cited by 6
- groupHomology.comp_d₃₂_eqproof · cited by 6
- groupCohomology.comp_d₂₃_eqproof · cited by 5
- groupCohomology.cochainsMap_f_0_comp_cochainsIso₀proof · cited by 4
- groupCohomology.cochainsMap_f_2_comp_cochainsIso₂proof · cited by 4
- ModuleCat.ExtendScalars.hom_extproof · cited by 4
- groupCohomology.d₀₁_comp_d₁₂proof · cited by 4