of_surjective

Mathlib.RingTheory.Finiteness.Basic

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

English

If f: A →+* B is surjective, then f is finite.

Русский

Если гомоморфизм f: A →+* B сюръективен, то он конечен.

LaTeX

$$$\\forall A B \, [\\text{CommRing } A] \, [\\text{CommRing } B], \\ f:A \to_+^* B, \\ Surjective f \Rightarrow f.Finite.$$$

Lean4

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

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

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

Разделы

Аффилиация

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