evalRingHom_apply — Mathlib

English

The evaluation homomorphism at j sends a restricted product element to its j-th coordinate.

Русский

Проведение evalRingHom в координате j отправляет элемент ограниченного произведения в его j-ю координату.

LaTeX

$$$\text{evalRingHom}_j(x) = x_j$$$

Lean4

@[simp]
theorem evalRingHom_apply [Π i, Ring (R i)] [∀ i, SubringClass (S i) (R i)] (x : Πʳ i, [R i, B i]_[𝓕]) (j : ι) :
    evalRingHom R j x = x j :=
  rfl

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