Theorems · Theorem · linear algebra

Module.lift_rank_bot_le_lift_rank_of_isScalarTower

∀ (R : Type u) (R' : Type u') [inst : Semiring R] [inst_1 : Semiring R'] (T : Type w) [inst_2 : Module R R']
  [inst_3 : NonAssocSemiring T] [inst_4 : Module R T] [inst_5 : Module R' T] [IsScalarTower R' T T] [FaithfulSMul R' T]
  [IsScalarTower R R' T], Cardinal.lift.{w, u'} (Module.rank R R') ≤ Cardinal.lift.{u', w} (Module.rank R T)

Defined in

Mathlib.LinearAlgebra.Dimension.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringSemiringModuleNonAssocSemiringModuleModuleIsScalarTowerFaithfulSMulIsScalarTower