Theorems · Theorem · commutative algebra

Module.Finite.of_equiv_equiv

∀ {A₁ : Type u_6} {B₁ : Type u_7} {A₂ : Type u_8} {B₂ : Type u_9} [inst : CommSemiring A₁] [inst_1 : CommSemiring B₁]
  [inst_2 : CommSemiring A₂] [inst_3 : Semiring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) → ∀ [Module.Finite A₁ B₁], Module.Finite A₂ B₂

See also Module.Finite.of_surjective and LinearMap.finite_iff_of_bijective.

Defined in

Mathlib.RingTheory.Finiteness.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringSemiringAlgebraAlgebraModule.Finite