map_add

Mathlib.Algebra.Ring.Hom.Defs

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

English

Ring homomorphisms preserve addition.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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