coe_add

Mathlib.FieldTheory.IntermediateField.Basic

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

English

Addition respects the underlying addition: the image of the sum equals the sum of the images.

Русский

Сложение сохраняется под отображением: образ суммы равен сумме образов.

LaTeX

$$$\bigl((x+y)\bigr) = x+y$$$

Lean4

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

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

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

Разделы

Аффилиация

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