monoidHom_injective — Mathlib

English

If each g i is an injective monoid homomorphism, then Pi.monoidHom g is injective.

Русский

Если каждый g i — инъективный моноид-гомоморфизм, то Pi.monoidHom g инъективна.

LaTeX

$$$ \text{Injective}(\Pi .\mathrm{monoidHom} \, g) $$$

Lean4

@[to_additive]
theorem monoidHom_injective {γ : Type w} [Nonempty I] [∀ i, MulOneClass (f i)] [MulOneClass γ] (g : ∀ i, γ →* f i)
    (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.monoidHom g) :=
  Pi.mulHom_injective (fun i => (g i).toMulHom) hg

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