cast_add

Mathlib.Data.Rat.Cast.CharZero

URI: https://scilib.ai/kg/mathlib#Rat.cast_add

← MathLib Explorer

English

For rationals p,q, the cast preserves addition: (p+q)↑ = p↑ + q↑.

Русский

Приведение суммы сохраняет сложение: (p+q)↑ = p↑ + q↑.

LaTeX

$$$ (p+q)^{\uparrow} = p^{\uparrow} + q^{\uparrow} $$$

Lean4

@[simp, norm_cast]
theorem cast_add (p q : ℚ) : ↑(p + q) = (p + q : α) :=
  cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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