finite_of_rank_eq_one

Mathlib.LinearAlgebra.Dimension.Finite

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

← MathLib Explorer

English

If M is free and has rank 1, then M is finite.

Русский

Если M свободен и имеет ранг 1, то M конечно.

LaTeX

$$[Module.Free R M] ∧ rank_R M = 1 ⇒ Module.Finite R M.$$

Lean4

theorem finite_of_rank_eq_one [Module.Free R M] (h : Module.rank R M = 1) : Module.Finite R M :=
  Module.finite_of_rank_eq_nat <| h.trans Nat.cast_one.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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