cast_divInt

Mathlib.Data.Rat.Cast.CharZero

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

English

For a,b ∈ ℤ, the cast of a/. b to α equals a / b in α.

Русский

Для a,b ∈ ℤ приведение a/. b к α равно a / b в α.

LaTeX

$$$ \big(a /. b\big)^{\uparrow} = a / b \quad (a,b \in \mathbb{Z}) $$$

Lean4

@[norm_cast]
theorem cast_divInt (a b : ℤ) : (a /. b : α) = a / b := by simp only [divInt_eq_div, cast_div, cast_intCast]

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

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

Разделы

Аффилиация

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