evalRingHom — Mathlib

English

There is a ring homomorphism from the restricted product to the coordinate component R_j, extending evalMonoidHom to rings.

Русский

Существует кольцевой гомоморфизм от ограниченного произведения к компоненте R_j, расширяющий evalMonoidHom до колец.

LaTeX

$$$\text{evalRingHom}_j: (\prod^r_i R_i) \to R_j, \quad x \mapsto x_j$ with ring structure preserved.$$

Lean4

/-- `RestrictedProduct.evalRingHom j` is the ring homomorphism from the restricted
product `Πʳ i, [R i, B i]_[𝓕]` to the component `R j`.
-/
def evalRingHom (j : ι) [Π i, Ring (R i)] [∀ i, SubringClass (S i) (R i)] : (Πʳ i, [R i, B i]_[𝓕]) →+* R j
    where
  __ := evalMonoidHom R j
  __ := evalAddMonoidHom R j

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