rank_eq_of_equiv_equiv — Mathlib

English

The same-universe version of rank equality under algebra equivalences asserts equality of ranks.

Русский

Та же вселенная версия равенства рангов при эквивалентностях алгебр утверждает равенство рангов.

LaTeX

$$$\operatorname{rank}_R S = \operatorname{rank}_{R'} S'$$$

Lean4

/-- The same-universe version of `Algebra.lift_rank_eq_of_equiv_equiv`. -/
theorem rank_eq_of_equiv_equiv (i : R ≃+* R') (j : S ≃+* S')
    (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) :
    Module.rank R S = Module.rank R' S' := by simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hc

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