finrank_eq_one — Mathlib

English

If R satisfies the strong rank condition and M is a free R-module of invertible type, then the finite rank of M is 1.

Русский

Пусть R удовлетворяет условию сильного ранга, и M — свободный R-модуль разрешимого типа; тогда его конечный размер равен 1.

LaTeX

$$$\operatorname{finrank}_R(M) = 1$$$

Lean4

theorem finrank_eq_one [StrongRankCondition R] [Free R M] : finrank R M = 1 :=
  by
  cases subsingleton_or_nontrivial R
  · rw [← rank_eq_one_iff_finrank_eq_one, rank_subsingleton]
  · rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, finrank_self]

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