coe_neg

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.coe_neg

English

The coe map preserves negation.

Русский

Встроение сохраняет отрицание.

LaTeX

$$$\\uparrow(-x) = -\\uparrow x$$$

Lean4

@[norm_cast]
theorem coe_neg : ∀ {x : ℚ}, (↑(-x) : ℚ_[p]) = -↑x :=
  Rat.cast_neg _

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

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

Разделы

Аффилиация

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