smul_pi₀ — Mathlib

English

If K is GroupWithZero and there is a MulAction on each R i, then for r ≠ 0, r • S.pi t = S.pi (r • t) (via Units).

Русский

Если K — GroupWithZero и действует на каждый R_i, то при r ≠ 0 выполняется r • S.pi t = S.pi (r • t) (через единицы).

LaTeX

$$$\\forall r \\in K, r \\neq 0 \\Rightarrow r \\cdot S.\\pi t = S.\\pi (r \\cdot t).$$$

Lean4

theorem smul_pi₀ [GroupWithZero K] [∀ i, MulAction K (R i)] {r : K} (S : Set ι) (t : ∀ i, Set (R i)) (hr : r ≠ 0) :
    r • S.pi t = S.pi (r • t) :=
  smul_pi (Units.mk0 r hr) S t

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