Theorems · Theorem · linear algebra

Module.finrank_baseChange

∀ {R : Type u} {S : Type u'} {M' : Type v'} [inst : Semiring R] [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid M']
  [StrongRankCondition R] [StrongRankCondition S] [inst_5 : Module S M'] [Module.Free S M'] [inst_7 : Algebra S R],
  Module.finrank R (TensorProduct S R M') = Module.finrank S M'

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringCommSemiringAddCommMonoidStrongRankConditionStrongRankConditionModuleModule.FreeAlgebra