Theorems · Theorem · linear algebra

rank_pi

∀ {R : Type u} {η : Type u₁'} {φ : η → Type u_1} [inst : Semiring R] [StrongRankCondition R]
  [inst_2 : (i : η) → AddCommMonoid (φ i)] [inst_3 : (i : η) → Module R (φ i)] [∀ (i : η), Module.Free R (φ i)]
  [Finite η], Module.rank R ((i : η) → φ i) = Cardinal.sum fun i => Module.rank R (φ i)

The rank of a finite product of free modules is the sum of the ranks.

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

6 results in Mathlib

Foundations

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

Assumes

SemiringStrongRankConditionAddCommMonoidModuleModule.FreeFinite