finrank_eq_one_iff — Mathlib

English

A finite free module has finrank equal to 1 iff there exists a basis indexed by a unique type.

Русский

Свободный конечный модуль имеет finrank = 1 тогда и только тогда, когда существует база, индексируемая уникальным типом.

LaTeX

$$$$ \\text{finrank}_R M = 1 \\;\\iff\\; \\exists ι:\\text{Basis } ι\\;R\\;M $$$$

Lean4

/-- A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.
-/
theorem finrank_eq_one_iff [Module.Free K V] (ι : Type*) [Unique ι] : finrank K V = 1 ↔ Nonempty (Basis ι K V) :=
  by
  constructor
  · intro h
    exact ⟨Module.basisUnique ι h⟩
  · rintro ⟨b⟩
    simpa using finrank_eq_card_basis b

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