Theorems · Theorem · linear algebra

Module.finrank_pi_fintype

∀ (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 ((i : ι) → M i) = ∑ i, Module.finrank R (M i)

The finrank of a finite product is the sum of the finranks.

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

6 results in Mathlib

Foundations

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

Assumes

SemiringStrongRankConditionFintypeAddCommMonoidModuleModule.FreeModule.Finite