Theorems · Theorem · commutative algebra
ModuleCat.free_shortExact_finrank_add
∀ {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
S.ShortExact →
∀ {n p : ℕ} [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃] [Module.Finite R ↑S.X₁] [Module.Finite R ↑S.X₃],
Module.finrank R ↑S.X₁ = n →
Module.finrank R ↑S.X₃ = p → ∀ [StrongRankCondition R], Module.finrank R ↑S.X₂ = n + p- Defined in
- Mathlib.Algebra.Category.ModuleCat.Free
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Cardinalproof · cited by 2,598
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- Module.finrankstatement and proof · cited by 1,770
- ModuleCatstatement and proof · cited by 1,429
- CategoryTheory.ShortComplex.X₂statement · cited by 1,115
- Module.Finitestatement and proof · cited by 1,032
- ModuleCat.carrierstatement and proof · cited by 997
- CategoryTheory.ShortComplex.X₁statement and proof · cited by 889
- CategoryTheory.ShortComplex.X₃statement and proof · cited by 876
- Module.Freestatement and proof · cited by 597
- Nat.cast_addproof · cited by 586
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.