degree_eq_of_mem_mem — Mathlib

English

If a nonzero element belongs to both components ℳ_i and ℳ_j, then i = j.

Русский

Если ненулевой элемент принадлежит обеим компонентам ℳ_i и ℳ_j, то i = j.

LaTeX

$$$x\in \mathcal{M}_i \cap \mathcal{M}_j \setminus \{0\} \Rightarrow i=j$$$

Lean4

theorem degree_eq_of_mem_mem {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) : i = j := by
  contrapose! hx; rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx]

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