single_mul_right — Mathlib

English

For a fixed index i and elements f ∈ ∀ i, α_i and a ∈ α_i, the equality single i (f(i) · a) = f · single i a holds in the Pi-type, i.e., the global factorization by the i-th coordinate.

Русский

Для фиксированного индекса i и элементов f, a выполняется равенство: single i (f(i) · a) = f · single i a.

LaTeX

$$$\forall a:\; \operatorname{single}_i(f(i)\cdot a) = f \cdot \operatorname{single}_i a.$$$

Lean4

theorem single_mul_right (a : α i) : single i (f i * a) = f * single i a :=
  funext fun _ ↦ single_mul_right_apply _ _ _ _

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