codisjoint_toSubmodule — Mathlib

English

Equivalence of codisjointness between LieSubmodules and their Submodules

Русский

Эквивалентность кодисjoint между Ли-подмодулями и их подмодулями

LaTeX

$$$\text{codisjoint}(N,N') \;\Longleftrightarrow\; \text{codisjoint}(N,N')$$$

Lean4

@[simp]
theorem codisjoint_toSubmodule : Codisjoint (N : Submodule R M) (N' : Submodule R M) ↔ Codisjoint N N' := by
  rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule, top_toSubmodule, ← codisjoint_iff]

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