toAddEquiv_toIntLinearEquiv — Mathlib

English

The linearization to Int and back preserves the underlying AddEquiv structure, i.e., mapping via toIntLinearEquiv and back via toAddEquiv is identity on AddEquiv.

Русский

Преобразование через toIntLinearEquiv и обратно через toAddEquiv оставляет AddEquiv без изменений.

LaTeX

$$$$ (e : M \\\\to_+ M_2) \\\\mapsto e.toIntLinearEquiv \\\\mapsto (e.toIntLinearEquiv).toAddMonoidHom \\\\\\text{ и обратно} = e $$$$

Lean4

@[simp]
theorem _root_.LinearEquiv.toAddEquiv_toIntLinearEquiv (e : M ≃ₗ[ℤ] M₂) : AddEquiv.toIntLinearEquiv (e : M ≃+ M₂) = e :=
  DFunLike.coe_injective rfl

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