disjoint_iff_comap_eq_bot — Mathlib

English

Two submodules p and q are disjoint iff the comap of p.subtype to q is the bottom submodule.

Русский

Два подмодуля p и q не пересекаются тогда и только тогда, когда comap p.subtype q равен нижнему подмодулю.

LaTeX

$$$\text{Disjoint } p\; q \iff comap\; p.subtype\; q = ⊥$$$

Lean4

theorem disjoint_iff_comap_eq_bot {p q : Submodule R M} : Disjoint p q ↔ comap p.subtype q = ⊥ := by
  rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff, map_comap_subtype,
    map_bot, disjoint_iff]

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