coe_toNatLinearEquiv — Mathlib

English

Let e be an additive equivalence between two AddCommMonoids M and M₂. Then the underlying map of its natural-number linearization coincides with e itself; in particular, the map e.toNatLinearEquiv has the same action as e.

Русский

Пусть e — аддитивное эквивалентное отображение между двумя коммутативными аддитивными группами M и M₂. Тогда поданная им ℕ-линейная биекция совпадает с e по значениям на элементах: ⇑e.toNatLinearEquiv = e.

LaTeX

$$$\\\\forall e : M \\\\simeq_+ M_2,\\\\ (e.toNatLinearEquiv).toFun = e$$$

Lean4

@[simp]
theorem coe_toNatLinearEquiv : ⇑e.toNatLinearEquiv = e :=
  rfl

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