quotient — Mathlib

English

If h is an IsTorsionBy in M by r, then the quotient module M/N inherits IsTorsionBy by r.

Русский

Если h� обладает торсионностью по r в M, то фактор-модуль M/N наследует торсионность по r.

LaTeX

$$$IsTorsionBy R M r \\Rightarrow IsTorsionBy R (M \\ slash N) r$$$

Lean4

theorem quotient (N : Submodule R M) {r : R} (h : IsTorsionBy R M r) : IsTorsionBy R (M ⧸ N) r :=
  (isTorsionBy_quotient_iff N r).mpr fun x => @h x ▸ N.zero_mem

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