ofReal_add

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofReal_add

English

For real r,s, the embedding preserves addition: (r+s : K) = (r : K) + (s : K).

Русский

Для действительных r, s отображение сохраняет сложение: (r+s : K) = (r : K) + (s : K).

LaTeX

$$$\bigl(r+s : K\bigr) = (r : K) + (s : K)$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_add (r s : ℝ) : ((r + s : ℝ) : K) = r + s :=
  algebraMap.coe_add _ _

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

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

Разделы

Аффилиация

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