smul_pi — Mathlib

English

If K is a Group and there is a MulAction of K on each R i, then for any r ∈ K, r • S.pi t = S.pi (r • t).

Русский

Если K — группа и существует действие умножения K на каждый R_i, то для любого r ∈ K выполняется r • S.pi t = S.pi (r • t).

LaTeX

$$$r \\cdot S.\\pi t = S.\\pi (r \\cdot t).$$$

Lean4

@[to_additive]
theorem smul_pi [Group K] [∀ i, MulAction K (R i)] (r : K) (S : Set ι) (t : ∀ i, Set (R i)) :
    r • S.pi t = S.pi (r • t) :=
  piMap_image_pi (fun _ _ => MulAction.surjective _) _

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