toNatLinearEquiv_symm

Mathlib.Algebra.Module.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#AddEquiv.toNatLinearEquiv_symm

English

For e : M ≃+ M₂, the Nat-linear symmetry e.toNatLinearEquiv.symm equals e.symm.toNatLinearEquiv.

Русский

Для e : M ≃+ M₂ симметрическая Nat-линейность равна соответствующей симметричной Nat-линейности e.symm.

LaTeX

$$$$ e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru