Theorems · Theorem · linear algebra

lift_rank_mul_lift_rank

∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A],
  Cardinal.lift.{w, v} (Module.rank F K) * Cardinal.lift.{v, w} (Module.rank K A) =
    Cardinal.lift.{v, w} (Module.rank F A)

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. The universe polymorphic version of rank_mul_rank below.

Defined in

Mathlib.LinearAlgebra.Dimension.Free

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommMonoidModuleModuleModuleIsScalarTowerStrongRankConditionStrongRankConditionModule.FreeModule.Free