finrank_of_not_finite

Mathlib.LinearAlgebra.Dimension.Free

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

← MathLib Explorer

English

If a free R-module M is not finite, then its finrank is 0.

Русский

Если свободный R-модуль M не конечен, то его финразмерность равна 0.

LaTeX

$$$$ \\lnot Module.Finite\\,R\\,M \\rightarrow finrank\\,R\\,M = 0 $$$$

Lean4

theorem finrank_of_not_finite (h : ¬Module.Finite R M) : finrank R M = 0 :=
  by
  rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff]
  exact .inr h

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

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

Разделы

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

Аффилиация

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