toRatLinearMap

Mathlib.Algebra.Module.LinearMap.Rat

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.toRatLinearMap

← MathLib Explorer

English

Reiteration of the linearity of addition on M × M.

Русский

Повторение линейности сложения на M × M.

LaTeX

$$IsLinearMap R (fun x : M × M => x.1 + x.2)$$

Lean4

/-- Reinterpret an additive homomorphism as a `ℚ`-linear map. -/
def toRatLinearMap [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) : M →ₗ[ℚ] M₂ :=
  { f with map_smul' := map_rat_smul f }

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

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

Разделы

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

Аффилиация

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