equiv — Mathlib

English

If A is of finite type over R and A ≃_R B is an algebra isomorphism, then B is also of finite type over R.

Русский

Если A имеет конечную презентацию над R, и есть алгебраическое эквивалентное отображение A ≃_R B, то B тоже имеет конечную презентацию над R.

LaTeX

$$$\\text{Algebra.FiniteType } R A \\to (A\\simeq_R B) \\Rightarrow \\text{Algebra.FiniteType } R B$$$

Lean4

theorem equiv (hRA : FiniteType R A) (e : A ≃ₐ[R] B) : FiniteType R B :=
  hRA.of_surjective e e.surjective

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