congrLinearEquiv_symm

Mathlib.LinearAlgebra.GeneralLinearGroup

URI: https://scilib.ai/kg/mathlib#LinearMap.GeneralLinearGroup.congrLinearEquiv_symm

English

The inverse of congrLinearEquiv e12 is congrLinearEquiv e12.symm.

Русский

Обратное congrLinearEquiv e12 равно congrLinearEquiv e12.symm.

LaTeX

$$$ (congrLinearEquiv e_{12}).\text{symm} = congrLinearEquiv e_{12}.symm $$$

Lean4

@[simp]
theorem congrLinearEquiv_symm (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) : (congrLinearEquiv e₁₂).symm = congrLinearEquiv e₁₂.symm :=
  rfl

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

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

Разделы

Аффилиация

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