map_mul — Mathlib

English

Reiterates that a monoid hom preserves multiplication.

Русский

Повторение: моноид-гомоморфизм сохраняет умножение.

LaTeX

$$$f(a b) = f(a) f(b)$$$

Lean4

/-- If `f` is a monoid homomorphism then `f (a * b) = f a * f b`. -/
@[to_additive /-- If `f` is an additive monoid homomorphism then `f (a + b) = f a + f b`. -/
    ]
protected theorem map_mul [MulOne M] [MulOne N] (f : M →* N) (a b : M) : f (a * b) = f a * f b :=
  f.map_mul' a b

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