Theorems · Theorem · linear algebra

Module.rank_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.rank S (M →ₗ[R] N) = Cardinal.lift.{w, v} (Module.rank R M) * Cardinal.lift.{v, w} (Module.rank S N)

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleModule.FreeModule.FiniteAddCommGroupModuleModuleSMulCommClassStrongRankConditionStrongRankConditionModule.Free