cast_sub

Mathlib.Data.Rat.Cast.CharZero

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

← MathLib Explorer

English

For rationals p,q, the cast preserves subtraction: (p−q)↑ = p↑ − q↑.

Русский

Приведение вычитания сохраняет разность: (p−q)↑ = p↑ − q↑.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_sub (p q : ℚ) : ↑(p - q) = (p - q : α) :=
  cast_sub_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