equiv — Mathlib

English

If there is an algebra isomorphism e: B ≃ₐ[A] B' with finite A–B structure, then finiteness transfers along the equivalence.

Русский

При наличии алгебраического изоморфизма между базовыми кольцами финитность переходит через эквиваленцию.

LaTeX

$$$\\forall (e: B \\cong_A B'),\\; [Module.Finite A B] \\Rightarrow [Module.Finite A B']$$

Lean4

theorem equiv [Module.Finite R M] (e : M ≃ₗ[R] N) : Module.Finite R N :=
  of_surjective (e : M →ₗ[R] N) e.surjective

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