cast — Mathlib

English

There is a canonical coercion term cast that sends an element of R into A via the algebra structure, i.e., the algebraCast is algebraMap.

Русский

Существет каноническое приведение, переводящее элемент из R в A через алгебраическую структуру (алгебраическая карта).

LaTeX

$$$\text{cast}: R \to A \text{ is given by } \text{algebraMap } R A.$$$

Lean4

/-- Coercion from a commutative semiring to an algebra over this semiring. -/
@[coe, reducible]
def cast {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] : R → A :=
  algebraMap R A

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