toFinset_nsmul — Mathlib

English

N-scalar multiplication preserves finset representation for nonzero n.

Русский

Умножение на не ноль n сохраняет представление Finset через toFinset.

LaTeX

$$$\forall s:\text{Multiset}(\alpha),\forall n\neq 0,\ (n \cdot s).toFinset = s.toFinset$$$

Lean4

@[simp]
theorem toFinset_nsmul (s : Multiset α) : ∀ n ≠ 0, (n • s).toFinset = s.toFinset
  | 0, h => by contradiction
  | n + 1, _ => by
    by_cases h : n = 0
    · rw [h, zero_add, one_nsmul]
    · rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]

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