eq_zero_of_coe_mem_of_disjoint — Mathlib

English

If p and q are disjoint submodules and a ∈ p, with a mapped to M, and a ∈ q, then a must be zero in p.

Русский

Если p и q — несовместимые подмодули и a ∈ p допускается как элемент M, и a ∈ q, тогда a = 0 в p.

LaTeX

$$$\\forall a \\in p,\\ (a \\in q) \\Rightarrow a = 0$$$

Lean4

theorem eq_zero_of_coe_mem_of_disjoint (hpq : Disjoint p q) {a : p} (ha : (a : M) ∈ q) : a = 0 :=
  mod_cast disjoint_def.mp hpq a (coe_mem a) ha

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