dedup_nsmul — Mathlib

English

For any α with decidable equality and any s, if n ≠ 0, then (n • s).dedup = s.dedup.

Русский

Для любого α с допускаемой равенством, и любого s, если n ≠ 0, то (n • s).dedup = s.dedup.

LaTeX

$$$\bigl(n \neq 0\bigr) \implies ( (n \cdot s)^{\mathrm{dedup}} = s^{\mathrm{dedup}} ).$$$

Lean4

@[simp]
theorem dedup_nsmul [DecidableEq α] {s : Multiset α} {n : ℕ} (hn : n ≠ 0) : (n • s).dedup = s.dedup := by ext a;
  by_cases h : a ∈ s <;> simp [h, hn]

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