ofReal_mul

Mathlib.Analysis.RCLike.Basic

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

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_mul (r s : ℝ) : ((r * s : ℝ) : K) = r * s :=
  algebraMap.coe_mul _ _

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

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

Разделы

Аффилиация

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