instOne

Mathlib.Algebra.Lie.Basic

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

English

There exists the identity Lie module equivalence on M, i.e., the identity map acts as the equivalence.

Русский

Существует идентичная эквивалентность Ли-модуля на M, то есть единичное отображение является этой эквивалентностью.

LaTeX

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

Lean4

instance : One (M ≃ₗ⁅R,L⁆ M) :=
  ⟨{ (1 : M ≃ₗ[R] M) with map_lie' := rfl }⟩

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

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

Разделы

Аффилиация

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