coeMonoidHom — Mathlib

English

The restricted product inherits a Group structure, with group operation defined componentwise and inverse taken coordinatewise.

Русский

Ограниченное произведение наследует структуру группы: операция группы по координатам, и обратная координатно.

LaTeX

$$$ (x \cdot y)_i = x_i \cdot y_i, \ (x^{-1})_i = x_i^{-1}. $$$

Lean4

/-- The coercion from the restricted product of monoids `A i` to the (normal) product
is a monoid homomorphism. -/
@[to_additive /-- The coercion from the restricted product of additive monoids `A i` to the
    (normal) product is an additive monoid homomorphism. -/
    ]
def coeMonoidHom [∀ i, Monoid (R i)] [∀ i, SubmonoidClass (S i) (R i)] : Πʳ i, [R i, B i]_[𝓕] →* Π i, R i
    where
  toFun := (↑)
  map_one' := rfl
  map_mul' _ _ := rfl

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