coe_add

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

The coe map from Q to Q_p preserves addition.

Русский

Встроение из Q в Q_p сохраняет операцию сложения.

LaTeX

$$$\\uparrow(x+y) = \\uparrow x + \\uparrow y$$$

Lean4

@[norm_cast]
theorem coe_add : ∀ {x y : ℚ}, (↑(x + y) : ℚ_[p]) = ↑x + ↑y :=
  Rat.cast_add _ _

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

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

Разделы

Аффилиация

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