one_lt_rank_of_one_lt_finrank

Mathlib.LinearAlgebra.Dimension.Finrank

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

English

If a module M has finrank_R M > 1, then its rank satisfies rank_R M > 1.

Русский

Если finrank_R M > 1, то rank_R M > 1.

LaTeX

$$$1 < \\mathrm{finrank}_R M \\Rightarrow 1 < \\mathrm{rank}_R M$$$

Lean4

theorem one_lt_rank_of_one_lt_finrank (h : 1 < finrank R M) : 1 < Module.rank R M := by
  simpa using lt_rank_of_lt_finrank h

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

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

Разделы

Аффилиация

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