linearDisjoint_comm_of_commute — Mathlib

English

If for all m ∈ M, n ∈ N we have Commute m n, then M.LinearDisjoint N if and only if N.LinearDisjoint M.

Русский

Если для всех m∈M, n∈N выполняется Commute m n, то M LinearDisjoint N эквив N LinearDisjoint M.

LaTeX

$$M.LinearDisjoint N \iff N.LinearDisjoint M \text{ under commuting assumption }$$

Lean4

/-- Linear disjointness is symmetric if elements in the module commute. -/
theorem linearDisjoint_comm_of_commute (hc : ∀ (m : M) (n : N), Commute m.1 n.1) :
    M.LinearDisjoint N ↔ N.LinearDisjoint M :=
  ⟨fun H ↦ H.symm_of_commute hc, fun H ↦ H.symm_of_commute fun _ _ ↦ (hc _ _).symm⟩

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