ofReal_neg

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofReal_neg

English

For any r ∈ ℝ, ((-r : ℝ) : K) = -r.

Русский

Для любого r ∈ ℝ, отображение (-r) в K равняется -r.

LaTeX

$$$((-r : \mathbb{R}) : K) = -r$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_neg (r : ℝ) : ((-r : ℝ) : K) = -r :=
  algebraMap.coe_neg r

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

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

Разделы

Аффилиация

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