coe_algebraMap — Mathlib

English

The canonical embedding of the base algebra maps to the skew monoid algebra aligns with the algebra map of A along the base map.

Русский

Каноническое вложение базовой алгебры согласуется с отображением алгебра-мэппинга A через основанное отображение.

LaTeX

$$$\text{coe}_{algebraMap}: algebraMap_k (SkewMonoidAlgebra A G) = (single 1) \circ algebraMap_k A$$$

Lean4

@[simp]
theorem coe_algebraMap [MulSemiringAction G A] [SMulCommClass G k A] :
    ⇑(algebraMap k (SkewMonoidAlgebra A G)) = single 1 ∘ algebraMap k A :=
  rfl

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