rank_inf_le_one_of_flat — Mathlib

English

If M and N are linearly disjoint, and at least one is flat, the intersection rank bound is ≤ 1, irrespective of commutativity constraints.

Русский

Если M и N линейно раздельны и хотя бы один из них плоский, ранг пересечения M ∩ N не превосходит 1.

LaTeX

$$Module.rank R ↥(M ⊓ N) ≤ 1$$

Lean4

/-- The `Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat`
for commutative rings. -/
theorem rank_inf_le_one_of_flat (hf : Module.Flat R M ∨ Module.Flat R N) : Module.rank R ↥(M ⊓ N) ≤ 1 :=
  H.rank_inf_le_one_of_commute_of_flat hf fun _ _ ↦ mul_comm _ _

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