coe_curry_symm

Mathlib.Algebra.Module.Equiv.Basic

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

English

The coercion of the inverse of curry equals uncurry at the function level.

Русский

Приведение к функции обратной от curry равняется uncurry на уровне функций.

LaTeX

$$$$ (LinearEquiv.curry R M V V_2)^{-1} = uncurry $$$$

Lean4

@[simp]
theorem coe_curry_symm : ⇑(LinearEquiv.curry R M V V₂).symm = uncurry :=
  rfl

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

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

Разделы

Аффилиация

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