mulMonoidHom — Mathlib

English

For commutative monoids α, the map (a,b) ↦ ab from α × α to α is a monoid homomorphism.

Русский

Для коммутативных моноидов α отображение (a,b) ↦ ab из α × α в α является моноид-гомоморфизмом.

LaTeX

$$$\\text{mulMonoidHom}: \\alpha \\times \\alpha \\to \\alpha$ with $\\text{mulMonoidHom}(a,b) = ab$ and $\\text{mulMonoidHom}$ respects multiplication.$$

Lean4

/-- Multiplication as a monoid homomorphism. -/
@[to_additive (attr := simps) /-- Addition as an additive monoid homomorphism. -/
    ]
def mulMonoidHom [CommMonoid α] : α × α →* α :=
  { mulMulHom with map_one' := mul_one _ }

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