Theorems · Theorem · linear algebra

Algebra.finrank_eq_of_equiv_equiv

∀ {R₀ : Type u_1} {S₀ : Type u_2} [inst : CommSemiring R₀] [inst_1 : Semiring S₀] [inst_2 : Algebra R₀ S₀]
  {R₁ : Type u_3} {S₁ : Type u_4} [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₀) →
    Module.finrank R₀ S₀ = Module.finrank 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 finrank of S₀ / R₀ is equal to the finrank of S₁ / R₁.

Defined in

Mathlib.LinearAlgebra.Dimension.Finrank

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraCommSemiringSemiringAlgebra