real_smul_eq_coe_smul

Mathlib.Analysis.RCLike.Basic

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

← MathLib Explorer

English

For any module E over K with a real structure, r • x = (r : K) • x.

Русский

Для любого модуля E над K с вещественным скалярным действием, верно r • x = (r : K) • x.

LaTeX

$$$r \cdot x = (r : K) \cdot x$$$

Lean4

theorem real_smul_eq_coe_smul [AddCommGroup E] [Module K E] [Module ℝ E] [IsScalarTower ℝ K E] (r : ℝ) (x : E) :
    r • x = (r : K) • x := by rw [RCLike.ofReal_alg, smul_one_smul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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