coe_add

Mathlib.Data.NNRat.Defs

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

English

The coercion from nonnegative rationals to rationals preserves addition: the coercion of p+q equals p+q as rationals.

Русский

Приведение из ℚ≥0 в ℚ сохраняет сложение: (p+q) в ℚ совпадает с p+q в ℚ.

LaTeX

$$$$ \big((p + q : \mathbb{Q}_{\ge 0}) : \mathbb{Q}\big) = p + q. $$$$

Lean4

@[simp, norm_cast]
theorem coe_add (p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q :=
  rfl

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

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

Разделы

Аффилиация

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