Theorems · Theorem · linear algebra

Module.finrank_directSum

∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] (M : ι → Type w)
  [inst_3 : (i : ι) → AddCommMonoid (M i)] [inst_4 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)]
  [∀ (i : ι), Module.Finite R (M i)], Module.finrank R (DirectSum ι fun i => M i) = ∑ i, Module.finrank R (M i)

The finrank of the direct sum is the sum of the finranks.

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

2 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringStrongRankConditionFintypeAddCommMonoidModuleModule.FreeModule.Finite