isAlgebraic — Mathlib

English

An algebraic isomorphism transfers IsAlgebraic between domains: if A and B are isomorphic as R-algebras and A is algebraic over R, then B is algebraic over R.

Русский

АлгЕquiv переносит алгебраичность через изоморфизм: если A и B изоморфны как R-алгебры и A алгебраичен над R, то B тоже алгебраичен над R.

LaTeX

$$$e: A ≃ₐ[R] B \;[\text{IsAlgebraic } R A] \Rightarrow \text{IsAlgebraic } R B$$$

Lean4

/-- Transfer `Algebra.IsAlgebraic` across an `AlgEquiv`. -/
theorem isAlgebraic (e : A ≃ₐ[R] B) [Algebra.IsAlgebraic R A] : Algebra.IsAlgebraic R B :=
  Algebra.IsAlgebraic.of_injective e.symm.toAlgHom e.symm.injective

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