toAddEquiv_toNatLinearEquiv — Mathlib

English

Let e : M ≃+ M₂. The map e.toNatLinearEquiv is an isomorphism of modules over ℕ, and its action recovers e when restricted appropriately.

Русский

Пусть e : M ≃+ M₂. Биекция e.toNatLinearEquiv является изоморфизмом модулей над ℕ и восстанавливает e в надлежащем ограничении.

LaTeX

$$$$ (e.toNatLinearEquiv) \\\\cong_? e $$$$

Lean4

@[simp]
theorem _root_.LinearEquiv.toAddEquiv_toNatLinearEquiv (e : M ≃ₗ[ℕ] M₂) : AddEquiv.toNatLinearEquiv ↑e = e :=
  DFunLike.coe_injective rfl

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