finrank_bot

Mathlib.LinearAlgebra.Dimension.Finite

URI: https://scilib.ai/kg/mathlib#finrank_bot

English

A finite-dimensional module has positive finrank iff there exists a nonzero vector.

Русский

У конечномерного модуля finrank > 0 тогда и только тогда, когда существует ненулевой вектор.

LaTeX

$$$0 < \operatorname{finrank} R M \;\iff\; \exists x \in M, x \neq 0$$$

Lean4

@[simp]
theorem finrank_bot : finrank R (⊥ : Submodule R M) = 0 :=
  finrank_eq_of_rank_eq (rank_bot _ _)

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

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

Разделы

Аффилиация

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