of_surjective

Mathlib.RingTheory.FiniteType

URI: https://scilib.ai/kg/mathlib#AlgHom.FiniteType.of_surjective

English

If f: A → B is a surjective R-algebra homomorphism, then B is a finite type algebra over A.

Русский

Если гомоморфизм f: A → B сюръективен, то B является алгеброй конечного типа над A.

LaTeX

$$$\\mathrm{Surjective}(f) \\Rightarrow \\mathrm{FiniteType}(f)$$$

Lean4

theorem of_surjective (f : A →ₐ[R] B) (hf : Surjective f) : f.FiniteType :=
  RingHom.FiniteType.of_surjective f.toRingHom hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru