symm_bijective

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleEquiv.symm_bijective

← MathLib Explorer

English

There is an identity Lie module equivalence on M.

Русский

Существует идентичная эквивалентность Ли-модуля на M.

LaTeX

$$$1_{M} : M \\simeq_{Lie} M$$$

Lean4

theorem symm_bijective : Function.Bijective (LieModuleEquiv.symm : (M ≃ₗ⁅R,L⁆ N) → N ≃ₗ⁅R,L⁆ M) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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