of'_eq_of — Mathlib

English

In presence of AddZeroClass M, the embedding of the additive structure via of' coincides with the standard embedding via of on the additive version of M.

Русский

При AddZeroClass M вложение через of' совпадает с обычным вложением через of для аддитивной версии M.

LaTeX

$$$\\mathrm{of'}\\ R\\ M a = \\mathrm{of}\\ R\\ M (\\;.\\mathrm{ofAdd} a\\.).$$$

Lean4

theorem of'_eq_of [AddZeroClass M] (a : M) : of' R M a = of R M (.ofAdd a) :=
  rfl

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