toLinearMap — Mathlib

English

Any R-algebra homomorphism is an R-linear map; it preserves addition and is linear over R.

Русский

Любой R-алгебрный гомоморфизм является линейным отображением над R; он сохраняет сложение и совместим с умножением на элементы R.

LaTeX

$$$\forall a,b \in A, \forall r \in R:\ φ(a+b)=φ(a)+φ(b) \quad\text{and}\quad φ(r a)=r\,φ(a).$$$

Lean4

/-- R-Alg ⥤ R-Mod -/
def toLinearMap : A →ₗ[R] B where
  toFun := φ
  map_add' := map_add _
  map_smul' := map_smul _

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