nontrivial_iff — Mathlib

English

Nontriviality of Submodule R M is equivalent to nontriviality of M itself.

Русский

Не тривиальность Submodule R M эквивалентна не тривиальности самого M.

LaTeX

$$$\\text{Nontrivial}(\\text{Submodule } R M) \\iff \\text{Nontrivial}(M)$$$

Lean4

@[simp]
theorem nontrivial_iff : Nontrivial (Submodule R M) ↔ Nontrivial M :=
  not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans <| subsingleton_iff R).trans not_nontrivial_iff_subsingleton.symm)

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