coe_toEquiv

Mathlib.Algebra.Module.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#LinearEquiv.coe_toEquiv

English

The function part of a semilinear equivalence equals the function obtained from the associated Equiv.

Русский

Функциональная часть семилинейной эквивалентности равна функции, полученной из ассоциированной эквивалентности.

LaTeX

$$toFun_eq_coe : e.toFun = EquivLike.toFunLike.coe e$$

Lean4

@[simp]
theorem coe_toEquiv : ⇑(e.toEquiv) = e :=
  rfl

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

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

Разделы

Аффилиация

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