finrank_eq_zero_of_rank_eq_zero

Mathlib.LinearAlgebra.Dimension.Finite

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

English

If the rank of a module M over R is zero, then finrank_R(M) is zero.

Русский

Если ранг модуля M над R равен нулю, то finrank_R(M) = 0.

LaTeX

$$$\\\\operatorname{finrank}_R M = 0 \\\\Leftarrow \\\\operatorname{Module.rank}_R M = 0.$$$

Lean4

theorem finrank_eq_zero_of_rank_eq_zero (h : Module.rank R M = 0) : finrank R M = 0 :=
  by
  delta finrank
  rw [h, zero_toNat]

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

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

Разделы

Аффилиация

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