mem_smul_iff_of_ne — Mathlib

English

If i ≠ j, then ⟨_, m₁⟩ lies in (of m₂) • w exactly when ⟨i,m₁⟩ lies in w.

Русский

Если i ≠ j, то элемент ⟨i,m₁⟩ лежит в (of m₂) • w тогда и только тогда, когда он лежит в w.

LaTeX

$$$$ \\langle i,m_1\\rangle \\in (of m_2 \\cdot w).toList \\iff \\langle i,m_1\\rangle \\in w.toList $$$$

Lean4

theorem mem_smul_iff_of_ne {i j : ι} (hij : i ≠ j) {m₁ : M i} {m₂ : M j} {w : Word M} :
    ⟨_, m₁⟩ ∈ (of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList := by simp [mem_smul_iff, *]

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