coe_add

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.coe_add

English

The inclusion map preserves addition: the image of the sum is the sum of the images.

Русский

Включение сохраняет сложение: образ суммы равен сумме образов.

LaTeX

$$$(x + y) = x + y$ in A, with x,y ∈ S$$

Lean4

protected theorem coe_add (x y : S) : (↑(x + y) : A) = ↑x + ↑y :=
  rfl

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

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

Разделы

Аффилиация

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