finite_of_finite — Mathlib

English

There exists n and S with a linear equivalence between (Fin n → R)/S and M.

Русский

Существует n и S, такие что (Fin n → R)/S эквивалентен по линейному отображению M.

LaTeX

$$$\\exists n \\exists S \\ Nonempty ((Fin n \to R) / S \\simeq_\\!{R} M).$$$

Lean4

theorem _root_.Module.finite_of_finite [Finite R] [Module.Finite R M] : Finite M := by
  obtain ⟨n, f, hf⟩ := exists_fin' R M; exact .of_surjective f hf

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