ofLinear_symm_apply

Mathlib.Algebra.Module.Equiv.Basic

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

English

The inverse of the isomorphism in the previous item, when applied to x ∈ M₂, yields g(x).

Русский

Обратное отображение данного изоморфизма, применённое к x ∈ M₂, даёт g(x).

LaTeX

$$$\bigl((ofLinear\ f\ g\ h_1\ h_2)^{-1}: M_2 \to M\bigr)(x) = g(x).$$$

Lean4

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

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

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

Разделы

Аффилиация

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