Theorems · Theorem · linear algebra

IsBaseChange.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 uM}
  [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 → Module.rank T P = Module.rank R M

Defined in

Mathlib.LinearAlgebra.Dimension.Localization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleCommRingNoZeroDivisorsAlgebraFaithfulSMulAddCommGroupModuleModuleIsScalarTower