zero_smul_finset — Mathlib

English

Statement about the smul by zero resulting in the zero Finset in the Finset framework.

Русский

Утверждение, что умножение нулём даёт нуль Finset.

LaTeX

$$$0\cdot s = 0$ for any Finset s.$$

Lean4

/-- A nonempty set is scaled by zero to the singleton set containing zero. -/
@[simp]
theorem zero_smul_finset {s : Finset β} (h : s.Nonempty) : (0 : α) • s = (0 : Finset β) :=
  coe_injective <| by simpa using @Set.zero_smul_set α _ _ _ _ _ h

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