surjective

Mathlib.Algebra.Ring.CompTypeclasses

URI: https://scilib.ai/kg/mathlib#RingHom.surjective

English

If a ring homomorphism σ: R1 → R2 is surjective, then as a function σ is surjective onto R2.

Русский

Если гомоморфизм σ: R1 → R2 сюръективен, то как функция σ образует surjectio на R2.

LaTeX

$$$\forall y \in R_2,\exists x \in R_1:\ σ(x) = y$$$

Lean4

theorem surjective (σ : R₁ →+* R₂) [t : RingHomSurjective σ] : Function.Surjective σ :=
  t.is_surjective

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

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

Разделы

Аффилиация

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