symm_of_commute — Mathlib

English

If M and N are linearly disjoint and every pair of elements m ∈ M and n ∈ N commute (mn = nm), then N is linearly disjoint with M.

Русский

Если M и N линейно несовместны и все пары элементов m∈M, n∈N commute, то N линейно несовместно с M.

LaTeX

$$H: M.LinearDisjoint N and ∀ m∈M, n∈N, Commute m n ⇒ N.LinearDisjoint M$$

Lean4

/-- Linear disjointness is symmetric if elements in the module commute. -/
theorem symm_of_commute (H : M.LinearDisjoint N) (hc : ∀ (m : M) (n : N), Commute m.1 n.1) : N.LinearDisjoint M :=
  by
  rw [linearDisjoint_iff, mulMap_comm_of_commute M N hc]
  exact ((TensorProduct.comm R N M).toEquiv.injective_comp _).2 H.injective

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