length_of_free_of_finite — Mathlib

English

If R is a ring with Strong Rank Condition and M is a finite free R-module, then length_R(M) = finrank_R(M) × length_R(R).

Русский

Если R удовлетворяет условию Strong Rank и M — конечный свободный модуль над R, то length_R(M) = finrank_R(M) × length_R(R).

LaTeX

$$$\operatorname{length}_R(M) = \operatorname{finrank}_R(M) \cdot \operatorname{length}_R(R)$$$

Lean4

theorem length_of_free_of_finite [StrongRankCondition R] [Module.Free R M] [Module.Finite R M] :
    Module.length R M = Module.finrank R M * Module.length R R := by
  rw [length_of_free, Cardinal.toENat_eq_nat.mpr (finrank_eq_rank _ _).symm]

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