Theorems · Theorem · linear algebra

Module.finrank_linearMap_self

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

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleModule.FreeModule.FiniteStrongRankConditionStrongRankConditionModuleSMulCommClass