factor_surjective — Mathlib

English

If S ⊆ T are two-sided ideals of a ring R, the canonical quotient map R/S → R/T is surjective.

Русский

Пусть S ⊆ T — двусторонние идеалы кольца R. Нормальное отображение R/S → R/T является сюръективным.

LaTeX

$$$\forall y \in R/T, \exists x \in R/S:\; (\text{factor } H)(x) = y$$$

Lean4

theorem factor_surjective (H : S ≤ T) : Function.Surjective (factor H) :=
  Ideal.Quotient.lift_surjective_of_surjective _ _ Ideal.Quotient.mk_surjective

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