Theorems · Theorem · linear algebra

IsBaseChange.lift_rank_eq

∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {T : Type uT}
  [inst_3 : CommRing T] [NoZeroDivisors T] [inst_5 : Algebra R T] [FaithfulSMul R T] {P : Type uP}
  [inst_7 : AddCommGroup P] [inst_8 : Module R P] [inst_9 : Module T P] [inst_10 : IsScalarTower R T P] {g : M →ₗ[R] P},
  IsBaseChange T g → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Defined in

Mathlib.LinearAlgebra.Dimension.Localization

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleCommRingNoZeroDivisorsAlgebraFaithfulSMulAddCommGroupModuleModuleIsScalarTower