ofReal_sub

Mathlib.Analysis.RCLike.Basic

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

English

For real r,s, ((r - s : ℝ) : K) = r - s.

Русский

Для действительных r и s: (r - s : K) = r - s.

LaTeX

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

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_sub (r s : ℝ) : ((r - s : ℝ) : K) = r - s :=
  map_sub (algebraMap ℝ K) r s

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

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

Разделы

Аффилиация

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