entryLinearMap_toAddMonoidHom — Mathlib

English

The linear map entryLinearMap R α i j, viewed as an AddMonoidHom, equals entryAddMonoidHom α i j.

Русский

Линейное отображение entryLinearMap R α i j, рассматриваемое как AddMonoidHom, равно entryAddMonoidHom α i j.

LaTeX

$$entryLinearMap R α i j : _ →+ _ = entryAddMonoidHom α i j$$

Lean4

@[simp]
theorem entryLinearMap_toAddMonoidHom {i : m} {j : n} : (entryLinearMap R α i j : _ →+ _) = entryAddMonoidHom α i j :=
  rfl

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