cast_mul

Mathlib.Data.Rat.Cast.CharZero

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

← MathLib Explorer

English

For rationals p,q, the cast preserves multiplication: (p·q)↑ = p↑ · q↑.

Русский

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

LaTeX

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

Lean4

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