rank_le_one_of_flat_of_self — Mathlib

English

If M is linearly disjoint from itself and M is flat as an R-module, then its rank is at most 1: rank_R(M) ≤ 1.

Русский

Если модуль M линейно взаимодиссоциирован с самим собой и плосок как модуль над R, тогда его ранг по R не превышает 1: rank_R(M) ≤ 1.

LaTeX

$$$\operatorname{rank}_R M \le 1$$$

Lean4

/-- The `Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self`
for commutative rings. -/
theorem rank_le_one_of_flat_of_self (H : M.LinearDisjoint M) [Module.Flat R M] : Module.rank R M ≤ 1 :=
  H.rank_le_one_of_commute_of_flat_of_self fun _ _ ↦ mul_comm _ _

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