toNatLinearEquiv_refl — Mathlib

English

For any M, theNat-linearization of the identity AddEquiv.refl M coincides with the identity LinearEquiv.refl ℕ M.

Русский

Для любого M линейное отображение, получаемое из идентичности AddEquiv.refl M, совпадает с идентичностью LinearEquiv.refl ℕ M.

LaTeX

$$$$ (AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl \\mathbb{N} M $$$$

Lean4

@[simp]
theorem toNatLinearEquiv_refl : (AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M :=
  rfl

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