of_apply — Mathlib

English

The embedding of AddMonoidAlgebra isomorphically maps an element a ∈ M to the basis element of R[M] at a with coefficient 1: of R M a = single a 1.

Русский

Вложение AddMonoidAlgebra изоморфно отображает элемент a ∈ M в базисный элемент R[M] на a с коэффициентом 1: of R M a = single a 1.

LaTeX

$$$\\mathrm{of}\\, R\\, M\\ a = \\mathrm{single}(a,1).$$$

Lean4

@[simp]
theorem of_apply [AddZeroClass M] (a : Multiplicative M) : of R M a = single a.toAdd 1 :=
  rfl

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