finite_of_finrank_pos

Mathlib.LinearAlgebra.Dimension.Free

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

English

If the finrank of M is positive, then M is finite.

Русский

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

LaTeX

$$$$ 0 < finrank\\,R\\,M \\rightarrow Module.Finite\\,R\\,M $$$$

Lean4

theorem finite_of_finrank_pos (h : 0 < finrank R M) : Module.Finite R M :=
  by
  contrapose h
  simp [finrank_of_not_finite h]

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

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

Разделы

Аффилиация

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