algebraMap — Mathlib

English

Given a commutative semiring R, a semiring A, and an R-algebra structure on A, there is a canonical embedding algebraMap: R →+* A sending r to its image in A under the algebra structure.

Русский

Существуют каноническое вложение algebraMap: R →+* A, отправляющее r в образ r в A через структуру алгебрации.

LaTeX

$$$\text{algebraMap}: R \to^+* A$ is the embedding given by the algebra structure on A.$$

Lean4

/-- Embedding `R →+* A` given by `Algebra` structure. -/
def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : R →+* A :=
  Algebra.algebraMap

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