toLinearMapClassRat

Mathlib.Algebra.Algebra.Rat

URI: https://scilib.ai/kg/mathlib#RingHomClass.toLinearMapClassRat

← MathLib Explorer

English

Cast-scalar smul equality for Rat: for q ∈ Rat and a in a Rat-module S, q.cast smul a equals the Rat smul q a.

Русский

Эквивалент выражения смула: q.cast смулит a так же, как q смулит a.

LaTeX

$$$$ q.cast \\cdot a = q \\cdot a $$$$

Lean4

instance _root_.RingHomClass.toLinearMapClassRat [FunLike F R S] [RingHomClass F R S] : LinearMapClass F ℚ R S where
  map_smulₛₗ f q a := by simp [smul_def, cast_id]

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

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

Разделы

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

Аффилиация

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