of_surjective

Mathlib.RingTheory.FiniteType

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

English

If a ring homomorphism is surjective, then it is of finite type.

Русский

Если кольцевой гомоморфизм сюръективен, то он имеет конечный тип.

LaTeX

$$of_surjective (f : RingHom A B) (hf : Surjective f) : f.FiniteType$$

Lean4

theorem of_surjective (f : A →+* B) (hf : Surjective f) : f.FiniteType :=
  by
  rw [← f.comp_id]
  exact (id A).comp_surjective hf

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

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

Разделы

Аффилиация

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