ofLinear_symm_toLinearMap

Mathlib.Algebra.Module.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#LinearEquiv.ofLinear_symm_toLinearMap

English

The inverse of the constructed linear equivalence corresponds to the map g.

Русский

Обратное к построенному линейному эквиваленту отображение соответствует g.

LaTeX

$$$(ofLinear\ f\ g\ h_1\ h_2)^{-1} = g$$$

Lean4

@[simp]
theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g :=
  rfl

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

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

Разделы

Аффилиация

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