free_shortExact_finrank_add — Mathlib

English

If X1 and X3 are finite (free) and the sequence is short exact with StrongRankCondition, then finrank(X2) = n + p when finrank(X1) = n and finrank(X3) = p.

Русский

Если X1 и X3 конечны и последовательность точна, то finrank(X2) = n + p при finrank(X1) = n и finrank(X3) = p.

LaTeX

$$$\text{finrank } R S.X_2 = n + p$ given $\text{finrank } R S.X_1 = n$ and $\text{finrank } R S.X_3 = p$ under StrongRankCondition$$

Lean4

theorem free_shortExact_finrank_add {n p : ℕ} [Module.Free R S.X₁] [Module.Free R S.X₃] [Module.Finite R S.X₁]
    [Module.Finite R S.X₃] (hN : Module.finrank R S.X₁ = n) (hP : Module.finrank R S.X₃ = p) [StrongRankCondition R] :
    finrank R S.X₂ = n + p := by
  apply finrank_eq_of_rank_eq
  rw [free_shortExact_rank_add hS', ← hN, ← hP]
  simp only [Nat.cast_add, finrank_eq_rank]

Похожие утверждения