reduceModIdeal_apply — Mathlib

English

The reduction mod I commutes with the action of f on representatives: (f.reduceModIdeal I)(Submodule.Quotient.mk (I • ⊤) x) = Submodule.Quotient.mk (I • ⊤) (f x).

Русский

сведение по I сохраняет действие f на представителях.

LaTeX

$$$\bigl(f \mathrm{.reduceModIdeal} I\bigr)(\mathrm{Submodule.Quotient.mk} (I \cdot \top) x) = \mathrm{Submodule.Quotient.mk} (I \cdot \top) (f x)$$$

Lean4

@[simp]
theorem reduceModIdeal_apply (f : M →ₗ[R] N) (x : M) :
    (f.reduceModIdeal I) (Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) x) =
      Submodule.Quotient.mk (p := (I • ⊤ : Submodule R N)) (f x) :=
  rfl

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