rank_inf_le_one_of_flat_left — Mathlib

English

Let R and S be commutative rings, and M,N submodules of S that are linearly disjoint over R. If M is flat as an R-module, then the rank of their intersection is at most 1: rank_R(M ∩ N) ≤ 1.

Русский

Пусть R и S — коммутативные кольца, M и N — подмодули S, линейно взаимно независимые над R. При этом M плоска как модуль над R. Тогда ранг пересечения M ∩ N по R не превосходит 1: rank_R(M ∩ N) ≤ 1.

LaTeX

$$$\operatorname{rank}_R\bigl(M \cap N\bigr) \le 1$$$

Lean4

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

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