map_add

Mathlib.Algebra.Algebra.NonUnitalHom

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

English

The constructed nonunital algebra hom from f with witnesses h1–h4 has underlying function f.

Русский

Сконструированный гомоморфизм без единицы из функции f имеет базовую функцию f.

LaTeX

$$$(\langle \langle \langle f,h_1\rangle,h_2,h_3\rangle,h_4\rangle) = f$$$

Lean4

protected theorem map_add (f : A →ₛₙₐ[φ] B) (x y : A) : f (x + y) = f x + f y :=
  map_add _ _ _

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

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

Разделы

Аффилиация

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