Theorems · Theorem · linear algebra

Module.finrank_prod

∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [StrongRankCondition R] [Module.Free R M] [Module.Free R M']
  [Module.Finite R M] [Module.Finite R M'], Module.finrank R (M × M') = Module.finrank R M + Module.finrank R M'

The finrank of M × M' is (finrank R M) + (finrank R M').

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleStrongRankConditionModule.FreeModule.FreeModule.FiniteModule.Finite