Theorems · Theorem · linear algebra

lift_rank_eq_of_equiv_equiv

∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] (i : R → R')
  (j : M ≃+ M'),
  Function.Bijective i →
    (∀ (r : R) (m : M), j (r • m) = i r • j m) →
      Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R' M')

If M / R and M' / R' are modules, i : R → R' is a bijective map which maps zero to zero, j : M ≃+ M' is a group isomorphism, such that the scalar multiplications on M and M' are compatible, then the rank of M / R is equal to the rank of M' / R'. As a special case, taking R = R' it is LinearEquiv.lift_rank_eq.

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

SemiringAddCommMonoidModuleSemiringAddCommMonoidModule