infinite — Mathlib

English

If M is infinite, then the quotient by the bottom submodule, M ⧸ (⊥), is infinite as well, since M ≅ M ⧸ ⊥.

Русский

Если M бесконечно, то фактор по нулевому подпространству ⊥, то есть M ⧸ ⊥, также бесконечен.

LaTeX

$$$$ \\text{If } \\lvert M \\rvert = \\infty, \\text{ then } \\lvert M / \\{0\\} \\rvert = \\infty.$$$$

Lean4

instance infinite [Infinite M] : Infinite (M ⧸ (⊥ : Submodule R M)) :=
  Infinite.of_injective Submodule.Quotient.mk fun _x _y h => sub_eq_zero.mp <| (Submodule.Quotient.eq ⊥).mp h

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