Theorems · Theorem · linear algebra

Module.finrank_matrix

∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] (m : Type u_2) (n : Type u_3) [inst_5 : Fintype m] [inst_6 : Fintype n],
  Module.finrank R (Matrix m n M) = Fintype.card m * Fintype.card n * Module.finrank R M

If m and n are Fintype, the finrank of m × n matrices over a module M is (Fintype.card m) * (Fintype.card n) * finrank R M.

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleStrongRankConditionModule.FreeFintypeFintype