coe_toLinearEquiv

Mathlib.Algebra.Lie.Basic

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

English

When viewing e as a linear equivalence over R, its underlying function is still e.

Русский

Когда e рассматривается как линейная эквивалентность над R, её базовая функция остается равной e.

LaTeX

$$$((e : M \\equiv_{R,L} N) : M \\equiv_R N)\\;:\\; M \\to N = e$$$

Lean4

@[simp]
theorem coe_toLinearEquiv (e : M ≃ₗ⁅R,L⁆ N) : ((e : M ≃ₗ[R] N) : M → N) = e :=
  rfl

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

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

Разделы

Аффилиация

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