ofLexLinearEquiv

Mathlib.Algebra.Order.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ofLexLinearEquiv

English

There is an α-linear isomorphism from Lex β to β, namely ofLexLinearEquiv.

Русский

Существует α-линейное изоморфное отображение от Lex β к β, namely ofLexLinearEquiv.

LaTeX

$$$\mathrm{Lex}(\beta) \cong_{\alpha} \beta$$$

Lean4

/-- `ofLex` as a linear equivalence -/
def ofLexLinearEquiv : Lex β ≃ₗ[α] β :=
  (ofLexAddEquiv β).toLinearEquiv ofLex_smul

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

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

Разделы

Аффилиация

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