map_mul

Mathlib.Algebra.Ring.Hom.Defs

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

English

Ring homomorphisms preserve multiplication.

Русский

Кольцевые гомоморфизмы сохраняют умножение.

LaTeX

$$$\forall a,b:\alpha,\ f(ab)=f(a)f(b)$$$

Lean4

/-- Ring homomorphisms preserve multiplication. -/
protected theorem map_mul (f : α →+* β) : ∀ a b, f (a * b) = f a * f b :=
  map_mul f

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

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

Разделы

Аффилиация

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