mul_apply — Mathlib

English

The restricted product inherits a coordinatewise multiplication from its factors: (x · y)_i = x_i · y_i.

Русский

Ограниченное произведение наследует покоординатное умножение от компонент: (x·y)_i = x_i · y_i.

LaTeX

$$$\\forall i,\\; (x \\cdot y)_i = x_i \\cdot y_i.$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_apply [Π i, Mul (R i)] [∀ i, MulMemClass (S i) (R i)] (x y : Πʳ i, [R i, B i]_[𝓕]) (i : ι) :
    (x * y) i = x i * y i :=
  rfl

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