codisjoint_iff — Mathlib

English

Codisjoint for p,q in f.invtSubmodule is equivalent to Codisjoint of p and q as submodules.

Русский

Codisjoint для p,q из f.invtSubmodule эквивалентен Codisjoint для p и q как подмодулей.

LaTeX

$$$\text{Codisjoint} p q \iff \text{Codisjoint}(p, q)$$$

Lean4

protected theorem codisjoint_iff {p q : f.invtSubmodule} :
    Codisjoint p q ↔ Codisjoint (p : Submodule R M) (q : Submodule R M) :=
  by
  obtain ⟨p, hp⟩ := p
  obtain ⟨q, hq⟩ := q
  simp

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