not_linearIndependent_pair_of_commute_of_flat

English

In a flat-right setting, any commuting pair in M ⊓ N cannot be linearly independent.

Русский

В ситуации плоского правого множества любая коммутирующая пара в M ∩ N не линейно независима.

LaTeX

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

Lean4

/-- If `M` and `N` are linearly disjoint, if one of `M` and `N` is flat, then any two commutative
elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`). -/
theorem not_linearIndependent_pair_of_commute_of_flat (hf : Module.Flat R M ∨ Module.Flat R N) (a b : ↥(M ⊓ N))
    (hc : Commute a.1 b.1) : ¬LinearIndependent R ![a, b] :=
  by
  rcases hf with _ | _
  · exact H.not_linearIndependent_pair_of_commute_of_flat_left a b hc
  · exact H.not_linearIndependent_pair_of_commute_of_flat_right a b hc

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