finrank_zero_iff_forall_zero — Mathlib

English

Let K be a division ring and V a finite-dimensional vector space over K. Then the dimension finrank_K V is 0 if and only if every vector in V is the zero vector.

Русский

Пусть K шаровая область, V конечномерное векторное пространство над K. Тогда finrank_K V = 0 тогда и только тогда, когда все векторы пространства равны нулю.

LaTeX

$$$\operatorname{finrank}_K(V) = 0 \iff \forall x \in V, x = 0$$$

Lean4

theorem finrank_zero_iff_forall_zero [FiniteDimensional K V] : finrank K V = 0 ↔ ∀ x : V, x = 0 :=
  Module.finrank_zero_iff.trans (subsingleton_iff_forall_eq 0)

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