coe_snd'

Mathlib.Topology.Algebra.Module.LinearMapPiProd

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_snd'

English

The function part of snd is the standard second projection map on the product, i.e., it equals Prod.snd.

Русский

Функциональная часть snd равна стандартной проекции на вторую координату, то есть Prod.snd.

LaTeX

$$$\uparrow(\mathrm{snd}\ R\ M_1\ M_2) = \mathrm{Prod.snd}.$$$

Lean4

@[simp, norm_cast]
theorem coe_snd' : ⇑(snd R M₁ M₂) = Prod.snd :=
  rfl

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

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

Разделы

Аффилиация

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