mk' — Mathlib

English

Let R be a semiring and M, M₂ be modules over R. If f: M → M₂ is a function that is linear, then there exists a linear map φ: M →ₗ[R] M₂ whose underlying function is f.

Русский

Пусть R — полукольцо, M и M₂ — модули над R. Пусть f: M → M₂ — произвольная функция, которая линейна. Тогда существует линейное отображение φ: M →ₗ[R] M₂, действующее как f на элементах.

LaTeX

$$$\exists \phi \in \mathrm{Hom}_R(M,M_2): \phi = f$$$

Lean4

/-- Convert an `IsLinearMap` predicate to a `LinearMap` -/
def mk' (f : M → M₂) (lin : IsLinearMap R f) : M →ₗ[R] M₂
    where
  toFun := f
  map_add' := lin.1
  map_smul' := lin.2

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