toLinearEquiv_symm

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.toLinearEquiv_symm

English

For every x, refl R1 M1 x = x.

Русский

Для каждого x: refl R1 M1 x = x.

LaTeX

$$$\text{refl}(R_1, M_1)(x) = x$$$

Lean4

@[simp]
theorem toLinearEquiv_symm (e : M₁ ≃SL[σ₁₂] M₂) : e.symm.toLinearEquiv = e.toLinearEquiv.symm :=
  rfl

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

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

Разделы

Аффилиация

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