isTorsionBy_quotient_iff — Mathlib

English

See isTorsionBy_quotient_iff above; it characterizes torsion by r in the quotient M/N.

Русский

См. выше isTorsionBy_quotient_iff; характеризует торсионность по r в фактор-модуле M/N.

LaTeX

$$$IsTorsionBy R (HasQuotient.Quotient M N) r \\iff \\forall x, SetLike.mem N (IsTorsionBy.hSMul r x)$$$

Lean4

theorem isTorsionBy_quotient_iff (N : Submodule R M) (r : R) : IsTorsionBy R (M ⧸ N) r ↔ ∀ x, r • x ∈ N :=
  Iff.trans N.mkQ_surjective.forall <| forall_congr' fun _ => Submodule.Quotient.mk_eq_zero N

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