quotOfMul — Mathlib

English

The map multiplying by a in the quotient by I lands in the quotient by a•I and is functorially compatible.

Русский

Отображение умножения на a в фактор-кольце по I переходит в фактор-кольцо по a•I и совместимо с отображениями.

LaTeX

$$Ideal.mulQuot a I$$

Lean4

/-- The quotient map `(R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span {a})`.
-/
def quotOfMul (a : R) (I : Ideal R) : (R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span { a }) :=
  Submodule.factor <| Submodule.singleton_set_smul I a ▸ Submodule.smul_le_span { a } I

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