map_mul

Mathlib.Algebra.GroupWithZero.Hom

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.map_mul

English

A zero-preserving monoid homomorphism preserves multiplication: f(a b) = f a · f b.

Русский

Гомоморфизм сохраняет произведение: f(a b) = f(a) f(b).

LaTeX

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

Lean4

protected theorem map_mul (f : α →*₀ β) (a b : α) : f (a * b) = f a * f b :=
  f.map_mul' a b

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru