evalMonoidHom_apply — Mathlib

English

There is a natural monoid homomorphism from the restricted product to the coordinate component R_j, given by projection onto the j-th factor.

Русский

Существует естественный моноид-гомоморфизм от ограниченного произведения в компоненту R_j, проекция на j-ю координату.

LaTeX

$$$\text{evMonoidHom}_j: (\prod^r_i R_i) \to R_j, \quad x \mapsto x_j.$$$

Lean4

@[simp]
theorem evalMonoidHom_apply [Π i, Monoid (R i)] [∀ i, SubmonoidClass (S i) (R i)] (x : Πʳ i, [R i, B i]_[𝓕]) (j : ι) :
    evalMonoidHom R j x = x j :=
  rfl

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