finite_iff_finite — Mathlib

English

If R is finite and M is finite as an R-module, then M is finite as a set.

Русский

Если R конечно и M конечно как R-модуль, то множество M конечно.

LaTeX

$$$[Finite R] \Rightarrow [Module.Finite R M] \Rightarrow Finite M.$$$

Lean4

/-- A module over a finite ring has finite dimension iff it is finite. -/
theorem _root_.Module.finite_iff_finite [Finite R] : Module.Finite R M ↔ Finite M :=
  ⟨fun _ ↦ finite_of_finite R, fun _ ↦ .of_finite⟩

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