flip_add

Mathlib.Analysis.Normed.Operator.Bilinear

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.flip_add

English

The canonical coercion of flipₗᵢ' is equal to the standard flip: the coercion map equals flip.

Русский

Отображение преобразования flipₗᵢ' в каноническую форму совпадает со стандартным flip.

LaTeX

$$$$ \operatorname{coe}(\text{flip}_{\ell i}') = \text{flip}. $$$$

Lean4

@[simp]
theorem flip_add (f g : E →SL[σ₁₃] F →SL[σ₂₃] G) : (f + g).flip = f.flip + g.flip :=
  rfl

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

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

Разделы

Аффилиация

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