Theorems · Theorem · linear algebra

rank_eq_of_equiv_equiv

∀ {R : Type u} {R' : Type u'} {M 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) → Module.rank R M = Module.rank R' M₁

The same-universe version of lift_rank_eq_of_equiv_equiv.

Defined in

Mathlib.LinearAlgebra.Dimension.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleSemiringAddCommMonoidModule