finrank_le_one_iff_isPrincipal — Mathlib

English

Let W be a submodule of V over K that is free and finite-dimensional. Then finrank K W ≤ 1 if and only if W is principal.

Русский

Пусть W — подпространство (подмодуль) V над K, обладающее вершиной свободы и конечной размерностью. Тогда finrank_K W ≤ 1 тогда и только тогда, когда W является порожденным одним элементом.

LaTeX

$$$\operatorname{finrank} K W \le 1 \iff W.\IsPrincipal$$$

Lean4

theorem finrank_le_one_iff_isPrincipal (W : Submodule K V) [Module.Free K W] [Module.Finite K W] :
    finrank K W ≤ 1 ↔ W.IsPrincipal := by rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

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