of_surjective

Mathlib.RingTheory.Finiteness.Basic

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

English

If f: A → B is a surjective ring homomorphism, then B is finite as an A-module.

Русский

Если f: A → B сюръективен, то B конечен как A-модуль.

LaTeX

$$$\\forall (f:\\, A \\to+* B),\\; \\text{Surjective } f \\Rightarrow \\text{Finite } A B$$$

Lean4

theorem of_surjective (f : A →+* B) (hf : Surjective f) : f.Finite :=
  letI := f.toAlgebra
  Module.Finite.of_surjective (Algebra.linearMap A B) hf

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

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

Разделы

Аффилиация

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