quotOfMul_surjective — Mathlib

English

The quotient map from R / (a I) to R / (span {a}) is surjective.

Русский

Картирование по частному кольцу от R / (a I) к R / (a) покрывающее.

LaTeX

$$Function.Surjective (Ideal.quotOfMul a I)$$

Lean4

/-- The quotient map `(R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span {a})` is surjective.
-/
theorem quotOfMul_surjective {a : R} (I : Ideal R) : Function.Surjective (Ideal.quotOfMul a I) :=
  by
  simp only [Ideal.quotOfMul]
  exact Submodule.factor_surjective <| Submodule.singleton_set_smul I a ▸ Submodule.smul_le_span { a } I

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