smul_univ — Mathlib

English

Pointwise smul distributes over Finset product in a family of Finsets indexed by i.

Русский

Пунктуальное умножение распространяется на произведение Finset в семействе Finset индексируемом по i.

LaTeX

$$$\\pi\\mathrm{Finset} (i \\mapsto s_i \\cdot t_i) = (\\pi\\mathrm{Finset} s_i) \\cdot (\\pi\\mathrm{Finset} t_i)$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_univ [Fintype β] {s : Finset α} (hs : s.Nonempty) : s • (univ : Finset β) = univ :=
  coe_injective <| by
    push_cast
    exact Set.smul_univ hs

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