rank_inf_le_one_of_flat_right — Mathlib

English

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

Русский

Пусть R и S — коммутативные кольца, M и N — подмодули S линейно взаимно независимы над R. Если N плоска как модуль над 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_right`
for commutative rings. -/
theorem rank_inf_le_one_of_flat_right [Module.Flat R N] : Module.rank R ↥(M ⊓ N) ≤ 1 :=
  H.rank_inf_le_one_of_commute_of_flat_right fun _ _ ↦ mul_comm _ _

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