rank_inf_le_one_of_commute_of_flat_right

English

The non-independence of any commuting pair in the flat-left or flat-right context holds under linear disjointness.

Русский

Несбалансированность любой коммутирующей пары в контексте плоскости слева или справа сохраняется при линейной несовместности.

LaTeX

$$¬LinearIndependent R ![a,b]$$

Lean4

/-- If `M` and `N` are linearly disjoint, if `N` is flat,
if any two elements of `↥(M ⊓ N)` are commutative, then the rank of `↥(M ⊓ N)` is at most one. -/
theorem rank_inf_le_one_of_commute_of_flat_right [Module.Flat R N] (hc : ∀ (m n : ↥(M ⊓ N)), Commute m.1 n.1) :
    Module.rank R ↥(M ⊓ N) ≤ 1 :=
  H.rank_inf_le_one_of_commute_of_flat (Or.inr ‹_›) hc

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