coe_flipₗᵢ'

Mathlib.Analysis.Normed.Operator.Bilinear

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

English

The function underlying flipₗᵢ' is the standard flip: ⇑(flipₗᵢ' ...) = flip.

Русский

Функция, лежащая в основе flipₗᵢ', равна стандартному flip: ⇑(flipₗᵢ' ...) = flip.

LaTeX

$$$$ \\text{coe\_flip}_{\\ell i}' = \\text{flip}. $$$$

Lean4

@[simp]
theorem coe_flipₗᵢ' : ⇑(flipₗᵢ' E F G σ₂₃ σ₁₃) = flip :=
  rfl

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

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

Разделы

Аффилиация

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