toIntLinearEquiv_refl — Mathlib

English

For e : M ≃+ M₂, the integer-linear equvialence e.toIntLinearEquiv, when considered as AddEquiv, equals e.

Русский

Для e : M ≃+ M₂ целочисленная линейная эквивалентность e.toIntLinearEquiv, рассматриваемая как AddEquiv, совпадает с e.

LaTeX

$$$$ ↑e.toIntLinearEquiv = e $$$$

Lean4

@[simp]
theorem toIntLinearEquiv_refl : (AddEquiv.refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M :=
  rfl

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