Theorems · Theorem · linear algebra

Algebra.lift_rank_eq_of_equiv_equiv

∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  {S' : Type v'} [inst_3 : CommSemiring R'] [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R ≃+* R')
  (j : S ≃+* S'),
  (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S) →
    Cardinal.lift.{v', v} (Module.rank R S) = Cardinal.lift.{v, v'} (Module.rank R' S')

If S / R and S' / R' are algebras, i : R ≃+* R' and j : S ≃+* S' are ring isomorphisms, such that R → R' → S' and R → S → S' commute, then the rank of S / R is equal to the rank of S' / R'.

Defined in

Mathlib.LinearAlgebra.Dimension.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraCommSemiringSemiringAlgebra