algebraMap_apply — Mathlib

English

The algebra map from R to the direct sum coincides with the embedding into the 0-th component via GAlgebra.toFun.

Русский

Алгебраическое отображение из R в прямую сумму совпадает с вложением в нулевой компонент через GAlgebra.toFun.

LaTeX

$$$\\mathrm{algebraMap}\\,R\\;\\big(\\bigoplus_i A_i\\big)\\;=\\;\\mathrm{DirectSum.of}\\,A\\,0\\;\\circ\\; (GAlgebra.toFun)$$$

Lean4

theorem algebraMap_apply (r : R) : algebraMap R (⨁ i, A i) r = DirectSum.of A 0 (GAlgebra.toFun r) :=
  rfl

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