coe_flipₗᵢ

Mathlib.Analysis.Normed.Operator.Bilinear

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_flipₗᵢ

English

The coercion of the flip map equals the standard flip map.

Русский

Приведение к функции разворота совпадает с обычной функцией разворота.

LaTeX

$$$ \\text{coe\_flip\\textsuperscript{∘}} = \\text{flip} $$$

Lean4

@[simp]
theorem coe_flipₗᵢ : ⇑(flipₗᵢ 𝕜 E Fₗ Gₗ) = flip :=
  rfl

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

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

Разделы

Аффилиация

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