finite_of_finrank_eq_succ

Mathlib.LinearAlgebra.Dimension.Free

URI: https://scilib.ai/kg/mathlib#Module.finite_of_finrank_eq_succ

English

If finrank R M equals n.succ for some n, then M is finite.

Русский

Если финразмерность модуля M равна n.succ, то M конечен.

LaTeX

$$$$ \\text{finrank}\\,R\\,M = n.succ \\rightarrow Module.Finite\\,R\\,M $$$$

Lean4

theorem finite_of_finrank_eq_succ {n : ℕ} (hn : finrank R M = n.succ) : Module.Finite R M :=
  finite_of_finrank_pos <| by rw [hn]; exact n.succ_pos

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru