rank_eq_of_equiv_equiv — Mathlib

English

If i and j define a compatible algebraic equivalence between two modules, then the ranks are equal.

Русский

Если существует совместимое алгебраическое эквивалентное соответствие между двумя модулями, то их ранги равны.

LaTeX

$$$\operatorname{rank}_R(M) = \operatorname{rank}_{R'}(M')$$$

Lean4

/-- The same-universe version of `lift_rank_eq_of_equiv_equiv`. -/
theorem rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M₁) (hi : Bijective i)
    (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : Module.rank R M = Module.rank R' M₁ := by
  simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hi hc

Похожие утверждения