rank_lt_rank_dual — Mathlib

English

Over a field K and a vector space V with aleph0 ≤ dim_K V, the dimension of V is strictly less than the dimension of the dual V* (in the standard sense).

Русский

Для поля K и пространства V с aleph0 ≤ dim_K V размерность V строго меньше размерности двойственного пространства V*.

LaTeX

$$$\aleph_0 \le \operatorname{rank}_K V \Rightarrow \operatorname{rank}_K V < \operatorname{rank}_K(V^*).$$$

Lean4

theorem rank_lt_rank_dual {K V : Type u} [Field K] [AddCommGroup V] [Module K V] (h : ℵ₀ ≤ Module.rank K V) :
    Module.rank K V < Module.rank K (V →ₗ[K] K) := by convert lift_rank_lt_rank_dual h; rw [lift_id]

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