coe_symm_toNatLinearEquiv — Mathlib

English

Let e be an additive equivalence M ≃+ M₂. Then the Nat-linear equivalence e.toNatLinearEquiv has as its inverse the Nat-linear equivalence corresponding to e.symm; i.e., e.toNatLinearEquiv.symm = (e.symm).toNatLinearEquiv.

Русский

Пусть e — аддитивное эквивалентное отображение M ≃+ M₂. Тогда обратное к e.toNatLinearEquiv совпадает с e.symm.toNatLinearEquiv.

LaTeX

$$$\\\\forall e : M \\\\simeq_+ M_2,\\\\ e.toNatLinearEquiv^{-1} = e^{-1}.toNatLinearEquiv$$$

Lean4

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

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