quotient — Mathlib

English

If hM is IsTorsionBySet R M s, then quotienting by N preserves IsTorsionBySet with the same set s.

Русский

Если hM является IsTorsionBySet R M s, то приведённое по N сохраняет IsTorsionBySet с тем же множеством s.

LaTeX

$$$IsTorsionBySet R (M/N) s$$$

Lean4

theorem quotient (N : Submodule R M) {s} (h : IsTorsionBySet R M s) : IsTorsionBySet R (M ⧸ N) s :=
  (isTorsionBySet_quotient_iff N s).mpr fun x r h' => @h x ⟨r, h'⟩ ▸ N.zero_mem

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