Theorems · Theorem · linear algebra

Module.finrank_linearMap

∀ (R : Type u) (S : Type u') (M : Type v) (N : Type w) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [inst_6 : AddCommGroup N] [inst_7 : Module R N]
  [inst_8 : Module S N] [inst_9 : SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S]
  [Module.Free S N], Module.finrank S (M →ₗ[R] N) = Module.finrank R M * Module.finrank S N

The finrank of M →ₗ[R] N as an S-module is (finrank R M) * (finrank S N).

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleModule.FreeModule.FiniteAddCommGroupModuleModuleSMulCommClassStrongRankConditionStrongRankConditionModule.Free