rank_eq_one_iff_finrank_eq_one

Mathlib.LinearAlgebra.Dimension.Finrank

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

← MathLib Explorer

English

If n ≥ 2, then rank_R M = n iff finrank_R M = n.

Русский

Если n ≥ 2, тогда rank_R M = n эквивалентно finrank_R M = n.

LaTeX

$$$$\\text{For } n \\geq 2,\\; \\operatorname{Module.rank}_R M = \\operatorname{OfNat.ofNat} n \\\\iff \\\\operatorname{finrank}_R M = \\operatorname{OfNat.ofNat} n.$$$$

Lean4

theorem rank_eq_one_iff_finrank_eq_one : Module.rank R M = 1 ↔ finrank R M = 1 :=
  Cardinal.toNat_eq_one.symm

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

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

Разделы

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

Аффилиация

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