isTorsionBySet_quotient_iff — Mathlib

English

For N and s, IsTorsionBySet R (M/N) s holds iff ∀ x ∈ M, ∀ r ∈ s, r • x ∈ N.

Русский

Для N и s: IsTorsionBySet R (M/N) s эквивалентно ∀ x∈M, ∀ r∈s, r•x ∈ N.

LaTeX

$$$IsTorsionBySet R (M/N) s \\iff \\forall x \\in M, \\forall r \\in s, r \\cdot x \\in N$$$

Lean4

theorem isTorsionBySet_quotient_iff (N : Submodule R M) (s : Set R) :
    IsTorsionBySet R (M ⧸ N) s ↔ ∀ x, ∀ r ∈ s, r • x ∈ N :=
  Iff.trans N.mkQ_surjective.forall <|
    forall_congr' fun _ => Iff.trans Subtype.forall <| forall₂_congr fun _ _ => Submodule.Quotient.mk_eq_zero N

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